:: SQUARE_1  semantic presentation begin  







scheme  :: SQUARE_1:sch 1 RealContinuity{ P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "z")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool P1[(Set (Var "x"))]) & (Bool P2[(Set (Var "y"))])) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z"))) & (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))  ")" )))
 provided
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool P1[(Set (Var "x"))]) & (Bool P2[(Set (Var "y"))])) "holds"  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))))
 proof 


end; definitionlet "x", "y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); :: original: :::"min"::: redefine func  :::"min":::  "(" "x" "," "y" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); :: original: :::"max"::: redefine func  :::"max":::  "(" "x" "," "y" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); end; 
theorem :: SQUARE_1:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y"))))) ; 
 
theorem :: SQUARE_1:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y"))))) ; 
 definitionlet "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func "x" :::"^2":::  ->    ($#m1_hidden :::"set"::: )   equals :: SQUARE_1:def 1 (Set "x"  ($#k3_xcmplx_0 :::"*"::: )  "x"); end; 





:: deftheorem    defines :::"^2"::: SQUARE_1:def 1 :  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x"))))); 
 registrationlet "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k3_square_1 :::"^2"::: )  ) ->   ($#v1_xcmplx_0 :::"complex"::: )   ; 
end; registrationlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k3_square_1 :::"^2"::: )  ) ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); :: original: :::"^2"::: redefine func "x" :::"^2":::  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); end; definitionlet "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); :: original: :::"^2"::: redefine func "x" :::"^2":::  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); end; 
theorem :: SQUARE_1:3 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: SQUARE_1:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" )))) ; 
 
theorem :: SQUARE_1:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" )))) ; 
 
theorem :: SQUARE_1:6 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))) ; 
 
theorem :: SQUARE_1:7 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" )  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))) ; 
 
theorem :: SQUARE_1:8 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" )))) ; 
 
theorem :: SQUARE_1:9 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" )))) ; 
 
theorem :: SQUARE_1:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )))) ; 
 
theorem :: SQUARE_1:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )))) ; 
 
theorem :: SQUARE_1:12 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: SQUARE_1:13 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) ; 
 
theorem :: SQUARE_1:14 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: SQUARE_1:15 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: SQUARE_1:16 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 definitionlet "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; assume 
(Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "a")))
 ; func  :::"sqrt"::: "a" ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   means :: SQUARE_1:def 2 (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  it) & (Bool (Set it  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  "a")  ")" ); end; 






:: deftheorem    defines :::"sqrt"::: SQUARE_1:def 2 :  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "holds"  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")))) "iff" (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b2"))) & (Bool (Set (Set (Var "b2"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )  ")" ))); 
 definitionlet "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); :: original: :::"sqrt"::: redefine func  :::"sqrt"::: "a" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); end; 
theorem :: SQUARE_1:17 (Bool (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 
theorem :: SQUARE_1:18 (Bool (Set   ($#k7_square_1 :::"sqrt"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: SQUARE_1:19 (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Num 2))) ; 
 
theorem :: SQUARE_1:20 (Bool (Set   ($#k7_square_1 :::"sqrt"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Num 2)) ; 
 
theorem :: SQUARE_1:21 (Bool (Set   ($#k7_square_1 :::"sqrt"::: )  (Num 2))  ($#r1_xxreal_0 :::"<"::: )  (Num 2)) ; 
 
theorem :: SQUARE_1:22 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: SQUARE_1:23 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: SQUARE_1:24 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: SQUARE_1:25 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a"))))) ; 
 
theorem :: SQUARE_1:26 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "y"))))) ; 
 
theorem :: SQUARE_1:27 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "y"))))) ; 
 
theorem :: SQUARE_1:28 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) ; 
 
theorem :: SQUARE_1:29 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: SQUARE_1:30 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: SQUARE_1:31 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool  "("  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) ; 
 
theorem :: SQUARE_1:32 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )))) ; 
 
theorem :: SQUARE_1:33 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )))) ; 
 
theorem :: SQUARE_1:34 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a"))))) ; 
 
theorem :: SQUARE_1:35 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b"))))) ; 
 
theorem :: SQUARE_1:36 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: SQUARE_1:37 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: SQUARE_1:38 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: SQUARE_1:39 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: SQUARE_1:40 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "y"))))  ")" )) ; 
 
theorem :: SQUARE_1:41 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))  ")" )) ; 
 
theorem :: SQUARE_1:42 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x")))) ; 
 
theorem :: SQUARE_1:43 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "(" (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" )) ; 
 begin  
theorem :: SQUARE_1:44 (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: SQUARE_1:45 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: SQUARE_1:46 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: SQUARE_1:47 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))  ")" )) ; 
 
theorem :: SQUARE_1:48 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))  ")" )) ; 
 
theorem :: SQUARE_1:49 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "holds"  (Bool (Set (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: SQUARE_1:50 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: SQUARE_1:51 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" )) ; 
 
theorem :: SQUARE_1:52 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" )) ; 
 
theorem :: SQUARE_1:53 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) ; 
 
theorem :: SQUARE_1:54 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: SQUARE_1:55 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ))) & (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )))  ")" )) ; 
 
theorem :: SQUARE_1:56 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )))) ; 
 
theorem :: SQUARE_1:57 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )))) ; 
 
theorem :: SQUARE_1:58 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b")))) ; 
 
theorem :: SQUARE_1:59 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" )))) ;