∀x∈ℚ ∃p,q∈ℤ ( q > 0 ∧ p = q·x ) [ℚ = ℤ/ℤ+]
  Given x ∈ ℚ:
    Let p', q' ∈ ℤ such that q' ≠ 0 ∧ p' = q'·x [ℚ = ℤ/ℤ*]
    If q' ∈ ℕ:
      q' ≥ 0
      q' > 0
      q' > 0 ∧ p' = q'·x
      ∃p,q∈ℤ ( q > 0 ∧ p = q·x )
    If –q ∈ ℕ:
      (–1)·p' = (–1)·q'·x
      –q' > 0 ∧ –p' = –q'·x
      ∃p,q∈ℤ ( q > 0 ∧ p = q·x )
    ∃p,q∈ℤ ( q > 0 ∧ p = q·x )
  ∀x∈ℚ ∃p,q∈ℤ ( q > 0 ∧ p = q·x )

If ∀x∈B∀y∈B∀z∈B(p(x)=p(y)∧p(y)=p(z)⇒x=y∨y=z∨z=x)
   Given a∈S
      If ¬∃x∈B(p(x)=a)
         Given d∈s
            If P(d)=a
               If ¬(d=a)
                  P(d)=a
                  ∃x∈B(p(x)=a)
                  ¬∃x∈B(p(x)=a)
                  ⊥
               d=a
               d=a∨d=a
            p(d)=a⇒d=a∨d=a
         ∀d∈B(p(d)=a⇒d=a∨d=a)
         ∀w∈B(p(w)=a⇒w=a∨w=a) [rename]
         ∃z∈B∀w∈B(p(w)=a⇒w=a∨w=z)
         ∃y∈B∃z∈B∀w∈B(p(w)=a⇒w=y∨w=z)

      If ∃x∈B(p(x)=a)
      Let b%S such that p(b)=a

∀x∈ℚ ∃p,q∈ℤ ( q > 0 ∧ p = q·x ∧ ∀d∈ℕ ( d | p,q ⇒ d = 1 ) ), where "d | p,q" is short-hand for "d | p ∧ d | q"
  Given x ∈ ℚ:
    ∃p,q∈ℤ ( q > 0 ∧ p = q·x ) [ℚ = ℤ/ℤ+]
    Let a, b ∈ ℤ such that b > 0 ∧ a = b·x
    Define P(m) ≡ m > 0 ∧ a = m·x
    ∃k∈ℕ ( P(k) ) ⇒ ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ) [well-ordering]
    b > 0 ∧ a = b·x
    ∃k∈ℕ ( k > 0 ∧ a = k·x )
    ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )
    Let m' ∈ ℕ such that P(m') ∧ ∀k∈ℕ ( P(k) ⇒ k≥m' )
    P(m')
    m' > 0 ∧ a = m'·x
    ∀k∈ℕ ( P(k) ⇒ k≥m' )

	::\ne ::≠
	::\le ::≤
	::\ge ::≥
	::\pm ::±
	::\nn ::ℕ
	::\zz ::ℤ
	::\qq ::ℚ
	::\rr ::ℝ
	::\cc ::ℂ
	::\pp ::ℙ

global escape:=true
messageoff:
	tooltip
return
message(text)
{
	tooltip % text
	settimer messageoff,-1000
}
LShift & RShift::
	escape:=!escape
	message( "Escape " ( escape ? "On" : "Off" ) )
return
#if escape
	::\ne ::≠
	::\le ::≤
	::\ge ::≥

Given x ∈ ℚ:
	Given d ∈ ℕ:
		If d | a ∧ d | m':
			If d > 1:
				a = 6
				m' = 3
				x = 2
				a = m'·x
				6 = 3·2

Given x ∈ ℚ:
  Given d ∈ ℕ:
    If d | a ∧ d | m':
      If d > 1:
        Let z ∈ ℕ such that a = d·z
        Let z' ∈ ℕ such that m' = d·z'
        a = m'·x = (d·z')·x
        d·z = (d·z')·x
        d·z = d·(z'·x)
        z = z'·x
        z' > 0
        z = z'·x ∧ z' > 0
        P(z')
        P(z') ⇒ z' ≥ m'
        z' ≥ m'
        z' < m'
        ⊥

  Given x ∈ ℚ:
    ∃p,q∈ℤ ( q > 0 ∧ p = q·x ) [ℚ = ℤ/ℤ+]
    Let a, b ∈ ℤ such that b > 0 ∧ a = b·x
    Define P(m) ≡ m > 0 ∧ a = m·x

Given x ∈ ℚ:
  Define P(k) ≡ k > 0 ∧ ∃j∈ℤ ( j = k·x ).

∀x∈ℚ ∃p,q∈ℤ ( q > 0 ∧ p = q·x ∧ ∀d∈ℕ ( d | p,q ⇒ d = 1 ) ), where "d | p,q" is short-hand for "d | p ∧ d | q"
  Given x ∈ ℚ:
    ∃p,q∈ℤ ( q > 0 ∧ p = q·x ) [ℚ = ℤ/ℤ+]
    Let a, b ∈ ℤ such that b > 0 ∧ a = b·x
    Define P(k) ≡ k > 0 ∧ ∃j∈ℤ ( j = k·x )
    ∃k∈ℕ ( P(k) ) ⇒ ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ) [well-ordering]
    b > 0 ∧ a = b·x
    a = b·x
    ∃j∈ℤ ( j = b·x )
    b > 0 ∧ ∃j∈ℤ ( j = b·x )
    P(b)
    ∃k∈ℕ ( P(k) )
    ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )
    Let m' ∈ ℕ such that P(m') ∧ ∀k∈ℕ ( P(k) ⇒ k≥m' )