:: EUCLID_3  semantic presentation begin  

















definitionlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"cpx2euc"::: "z" ->   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) equals :: EUCLID_3:def 1 (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k3_complex1 :::"Re"::: )  "z" ")" ) "," (Set  "("  ($#k4_complex1 :::"Im"::: )  "z" ")" ) ($#k19_euclid :::"]|"::: ) ); end; 





:: deftheorem    defines :::"cpx2euc"::: EUCLID_3:def 1 :  (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" ) "," (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" ) ($#k19_euclid :::"]|"::: ) ))); 
 definitionlet "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); func  :::"euc2cpx"::: "p" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: EUCLID_3:def 2 (Set (Set  "(" "p"  ($#k17_euclid :::"`1"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" "p"  ($#k18_euclid :::"`2"::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )); end; 





:: deftheorem    defines :::"euc2cpx"::: EUCLID_3:def 2 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))); 
 
theorem :: EUCLID_3:1 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k2_euclid_3 :::"euc2cpx"::: )  (Set  "("  ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "z")))) ; 
 
theorem :: EUCLID_3:2 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k1_euclid_3 :::"cpx2euc"::: )  (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) ; 
 
theorem :: EUCLID_3:3 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z2"))))) "holds"  (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "z2")))) ; 
 
theorem :: EUCLID_3:4 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p1")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p2"))))) "holds"  (Bool (Set (Var "p1"))  ($#r1_hidden :::"="::: )  (Set (Var "p2")))) ; 
 
theorem :: EUCLID_3:5 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k1_euclid_3 :::"cpx2euc"::: )  (Set  "(" (Set (Var "x1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "x2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k19_euclid :::"]|"::: ) ))) ; 
 
theorem :: EUCLID_3:6 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z2")) ")" ) ")" ) "," (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z2")) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; 
 
theorem :: EUCLID_3:7 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_euclid_3 :::"cpx2euc"::: )  (Set  "(" (Set (Var "z1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z2")) ")" )))) ; 
 
theorem :: EUCLID_3:8 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p2")) ")" )  ($#k17_euclid :::"`1"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p2")) ")" )  ($#k18_euclid :::"`2"::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))) ; 
 
theorem :: EUCLID_3:9 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k2_euclid_3 :::"euc2cpx"::: )  (Set  "(" (Set (Var "p1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p1")) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p2")) ")" )))) ; 
 
theorem :: EUCLID_3:10 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "z")) ")" ) ")" ) "," (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "z")) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" ) ")" ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; 
 
theorem :: EUCLID_3:11 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_euclid_3 :::"cpx2euc"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: EUCLID_3:12 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "p")) ")" )  ($#k17_euclid :::"`1"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "p")) ")" )  ($#k18_euclid :::"`2"::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))) ; 
 
theorem :: EUCLID_3:13 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k2_euclid_3 :::"euc2cpx"::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p")) ")" )))) ; 
 
theorem :: EUCLID_3:14 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_euclid_3 :::"cpx2euc"::: )  (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z1")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z2")) ")" )))) ; 
 
theorem :: EUCLID_3:15 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k2_euclid_3 :::"euc2cpx"::: )  (Set  "(" (Set (Var "p1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p1")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p2")) ")" )))) ; 
 
theorem :: EUCLID_3:16 (Bool (Set   ($#k1_euclid_3 :::"cpx2euc"::: )  (Set  ($#k5_complex1 :::"0c"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) ; 
 
theorem :: EUCLID_3:17 (Bool (Set   ($#k2_euclid_3 :::"euc2cpx"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) ; 
 
theorem :: EUCLID_3:18 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) ; 
 
theorem :: EUCLID_3:19 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k1_euclid_3 :::"cpx2euc"::: )  (Set  "(" (Set (Var "r"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "("  ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: EUCLID_3:20 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k2_euclid_3 :::"euc2cpx"::: )  (Set  "(" (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: EUCLID_3:21 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))) ; 
 
theorem :: EUCLID_3:22 (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Num 2))) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Num 1) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Num 2) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))) ; 
 
theorem :: EUCLID_3:23 (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Num 2)) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "f")))) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) )))) ; 
 
theorem :: EUCLID_3:24 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "("  ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))) ; 
 
theorem :: EUCLID_3:25 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ))) ; 
 definitionlet "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); func  :::"Arg"::: "p" ->   ($#m1_subset_1 :::"Real":::) equals :: EUCLID_3:def 3 (Set   ($#k1_comptrig :::"Arg"::: )  (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  "p" ")" )); end; 





:: deftheorem    defines :::"Arg"::: EUCLID_3:def 3 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_comptrig :::"Arg"::: )  (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p")) ")" )))); 
 
theorem :: EUCLID_3:26 (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p")))) "or" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_euclid_3 :::"cpx2euc"::: )  (Set (Var "z"))))  ")" )) "holds"  (Bool (Set   ($#k1_comptrig :::"Arg"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p")))))) ; 
 
theorem :: EUCLID_3:27 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "("  ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p")) ")" ) ")" ))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "("  ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p")) ")" ) ")" )))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k19_euclid :::"]|"::: ) )))) ; 
 
theorem :: EUCLID_3:28 (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 
theorem :: EUCLID_3:29 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "holds"  (Bool  "("   "("  (Bool (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k32_sin_cos :::"PI"::: )  ))) "implies" (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) )))  ")"  &  "("  (Bool (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k32_sin_cos :::"PI"::: )  ))) "implies" (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) )))  ")"   ")" )) ; 
 
theorem :: EUCLID_3:30 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: EUCLID_3:31 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "holds"  (Bool  "("  (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k32_sin_cos :::"PI"::: )  )) "iff" (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "p")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k32_sin_cos :::"PI"::: )  ))  ")" )) ; 
 
theorem :: EUCLID_3:32 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("  (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) "or" (Bool (Set (Set (Var "p1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set  "(" (Set (Var "p1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k32_sin_cos :::"PI"::: )  )) "iff" (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set  "(" (Set (Var "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k32_sin_cos :::"PI"::: )  ))  ")" )) ; 
 
theorem :: EUCLID_3:33 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "iff" (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: EUCLID_3:34 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p1")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k32_sin_cos :::"PI"::: )  )) & (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set (Var "p2")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k32_sin_cos :::"PI"::: )  ))) "holds"  (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set  "(" (Set (Var "p1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p2")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k32_sin_cos :::"PI"::: )  ))) ; 
 definitionlet "p1", "p2", "p3" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); func  :::"angle":::  "(" "p1" "," "p2" "," "p3" ")"  ->   ($#m1_subset_1 :::"Real":::) equals :: EUCLID_3:def 4 (Set   ($#k4_complex2 :::"angle"::: )   "(" (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  "p1" ")" ) "," (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  "p2" ")" ) "," (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  "p3" ")" ) ")" ); end; 







:: deftheorem    defines :::"angle"::: EUCLID_3:def 4 :  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex2 :::"angle"::: )   "(" (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p1")) ")" ) "," (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p2")) ")" ) "," (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p3")) ")" ) ")" ))); 
 
theorem :: EUCLID_3:35 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set  "(" (Set (Var "p1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" ) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" ) ")" ))) ; 
 
theorem :: EUCLID_3:36 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set  "(" (Set (Var "p1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_euclid_3 :::"Arg"::: )  (Set  "(" (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" ))) & (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: EUCLID_3:37 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")"  ")" )))) ; 
 
theorem :: EUCLID_3:38 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")"  ")" )))) ; 
 
theorem :: EUCLID_3:39 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "x"))  ($#k1_complex2 :::".|."::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "y")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "y")) ")" ) ")" )))) ; 
 
theorem :: EUCLID_3:40 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "x"))  ($#k1_complex2 :::".|."::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "y")) ")" ) ")" )))) ; 
 
theorem :: EUCLID_3:41 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )))) ; 
 
theorem :: EUCLID_3:42 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p1")) ")" )  ($#k1_complex2 :::".|."::: )  (Set  "("  ($#k2_euclid_3 :::"euc2cpx"::: )  (Set (Var "p2")) ")" ) ")" )))) ; 
 
theorem :: EUCLID_3:43 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "holds"  (Bool  "("  (Bool (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) "," (Set (Var "p2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2))) "or" (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) "," (Set (Var "p2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) )))  ")" )  ")" )) ; 
 
theorem :: EUCLID_3:44 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))) "holds"   "("  (Bool  "("  (Bool  "("  (Bool (Bool  "not" (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p1")) ($#k12_euclid :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p2")) ($#k12_euclid :::".|"::: ) )))) & (Bool (Bool  "not" (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p1")) ($#k12_euclid :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p2")) ($#k12_euclid :::".|"::: ) ) ")" ))))  ")" ) "or" (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) "," (Set (Var "p2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2))) "or" (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) "," (Set (Var "p2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) )))  ")" ) & (Bool  "("  (Bool  "("  (Bool (Bool  "not" (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) "," (Set (Var "p2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2)))) & (Bool (Bool  "not" (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) "," (Set (Var "p2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ))))  ")" ) "or" (Bool (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p1")) ($#k12_euclid :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p2")) ($#k12_euclid :::".|"::: ) ))) "or" (Bool (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p1")) ($#k12_euclid :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p2")) ($#k12_euclid :::".|"::: ) ) ")" )))  ")" )  ")" ) ; 
 
theorem :: EUCLID_3:45 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2")))) "holds"  (Bool  "("  (Bool (Set  ($#k23_rvsum_1 :::"|("::: ) (Set  "(" (Set (Var "p1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" ) "," (Set  "(" (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2))) "or" (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) )))  ")" )  ")" )) ; 
 
theorem :: EUCLID_3:46 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool  "("  (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k32_sin_cos :::"PI"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2))) "or" (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) )))  ")" )) "holds"  (Bool (Set (Set  "(" (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "p1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "p1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  ))) ; 
 
theorem :: EUCLID_3:47 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p1"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p3"))) & (Bool (Set (Var "p3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set   ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "p3")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k32_sin_cos :::"PI"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "p3")) ")"  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")"  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k4_euclid_3 :::"angle"::: )   "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k32_sin_cos :::"PI"::: )  ))) ; 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "p1", "p2", "p3" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); func  :::"Triangle":::  "(" "p1" "," "p2" "," "p3" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) equals :: EUCLID_3:def 5 (Set (Set  "(" (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" "p1" "," "p2" ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" "p2" "," "p3" ")"  ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" "p3" "," "p1" ")"  ")" )); end; 








:: deftheorem    defines :::"Triangle"::: EUCLID_3:def 5 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k5_euclid_3 :::"Triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p2")) "," (Set (Var "p3")) ")"  ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p3")) "," (Set (Var "p1")) ")"  ")" ))))); 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "p1", "p2", "p3" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); func  :::"closed_inside_of_triangle":::  "(" "p1" "," "p2" "," "p3" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) equals :: EUCLID_3:def 6  "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) : (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a1"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a2"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a3"))) & (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  "p1" ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  "p2" ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  "p3" ")" )))  ")" ))  "}"  ; end; 








:: deftheorem    defines :::"closed_inside_of_triangle"::: EUCLID_3:def 6 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k6_euclid_3 :::"closed_inside_of_triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a1"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a2"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a3"))) & (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p3")) ")" )))  ")" ))  "}"  ))); 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "p1", "p2", "p3" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); func  :::"inside_of_triangle":::  "(" "p1" "," "p2" "," "p3" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) equals :: EUCLID_3:def 7 (Set (Set  "("  ($#k6_euclid_3 :::"closed_inside_of_triangle"::: )   "(" "p1" "," "p2" "," "p3" ")"  ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "("  ($#k5_euclid_3 :::"Triangle"::: )   "(" "p1" "," "p2" "," "p3" ")"  ")" )); end; 








:: deftheorem    defines :::"inside_of_triangle"::: EUCLID_3:def 7 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k7_euclid_3 :::"inside_of_triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_euclid_3 :::"closed_inside_of_triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")"  ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "("  ($#k5_euclid_3 :::"Triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")"  ")" ))))); 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "p1", "p2", "p3" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); func  :::"outside_of_triangle":::  "(" "p1" "," "p2" "," "p3" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) equals :: EUCLID_3:def 8  "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) : (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Var "a1"))) "or" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Var "a2"))) "or" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Var "a3")))  ")" ) & (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  "p1" ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  "p2" ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  "p3" ")" )))  ")" ))  "}"  ; end; 








:: deftheorem    defines :::"outside_of_triangle"::: EUCLID_3:def 8 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k8_euclid_3 :::"outside_of_triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Var "a1"))) "or" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Var "a2"))) "or" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Var "a3")))  ")" ) & (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p3")) ")" )))  ")" ))  "}"  ))); 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "p1", "p2", "p3" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); func  :::"plane":::  "(" "p1" "," "p2" "," "p3" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) equals :: EUCLID_3:def 9 (Set (Set  "("  ($#k8_euclid_3 :::"outside_of_triangle"::: )   "(" "p1" "," "p2" "," "p3" ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k6_euclid_3 :::"closed_inside_of_triangle"::: )   "(" "p1" "," "p2" "," "p3" ")"  ")" )); end; 








:: deftheorem    defines :::"plane"::: EUCLID_3:def 9 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_euclid_3 :::"outside_of_triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k6_euclid_3 :::"closed_inside_of_triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")"  ")" ))))); 
 
theorem :: EUCLID_3:48 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ))) "holds"  (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p3")) ")" )))  ")" )))) ; 
 
theorem :: EUCLID_3:49 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k5_euclid_3 :::"Triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k6_euclid_3 :::"closed_inside_of_triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )))) ; 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "q1", "q2" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); pred "q1" "," "q2" :::"are_lindependent2":::  means :: EUCLID_3:def 10 (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  "q1" ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  "q2" ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "a1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )); end; 






:: deftheorem    defines :::"are_lindependent2"::: EUCLID_3:def 10 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "q1")) "," (Set (Var "q2"))  ($#r1_euclid_3 :::"are_lindependent2"::: )  ) "iff" (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "q1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "q2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "a1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))  ")" ))); 
 notationlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "q1", "q2" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); antonym "q1" "," "q2" :::"are_ldependent2":::  for "q1" "," "q2" :::"are_lindependent2"::: ; end; 
theorem :: EUCLID_3:50 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "q1")) "," (Set (Var "q2"))  ($#r1_euclid_3 :::"are_lindependent2"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q2"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )))  ")" ))) ; 
 
theorem :: EUCLID_3:51 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p0")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Set (Var "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1"))) "," (Set (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  ) & (Bool (Set (Var "p0"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ))) "holds"  (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "p0"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p3")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "p0"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "b1"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b2"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b3"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p3")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "b1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "a1"))) & (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Var "a2"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Var "a3")))  ")" )  ")" )  ")" )))) ; 
 
theorem :: EUCLID_3:52 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p0")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "p0"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p3")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" ))) "holds"  (Bool (Set (Var "p0"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )))) ; 
 
theorem :: EUCLID_3:53 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p3")) ")" )))  ")" ))  "}"  ))) ; 
 
theorem :: EUCLID_3:54 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Set (Var "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1"))) "," (Set (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  )) "holds"  (Bool (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_euclid :::"REAL"::: )  (Num 2)))) ; 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "p1", "p2", "p3", "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); assume 
(Bool  "("  (Bool (Set (Set (Const "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Const "p1"))) "," (Set (Set (Const "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Const "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  ) & (Bool (Set (Const "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Const "p1")) "," (Set (Const "p2")) "," (Set (Const "p3")) ")" ))  ")" )
 ; func  :::"tricord1":::  "(" "p1" "," "p2" "," "p3" "," "p" ")"  ->   ($#m1_subset_1 :::"Real":::) means :: EUCLID_3:def 11 (Bool  "ex" (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Set  "(" it  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool "p"  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" it  ($#k1_rlvect_1 :::"*"::: )  "p1" ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  "p2" ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  "p3" ")" )))  ")" )); end; 










:: deftheorem    defines :::"tricord1"::: EUCLID_3:def 11 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Set (Var "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1"))) "," (Set (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  ) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ))) "holds"  (Bool  "for" (Set (Var "b6")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_euclid_3 :::"tricord1"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )) "iff" (Bool  "ex" (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "b6"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "b6"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p3")) ")" )))  ")" ))  ")" )))); 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "p1", "p2", "p3", "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); assume 
(Bool  "("  (Bool (Set (Set (Const "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Const "p1"))) "," (Set (Set (Const "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Const "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  ) & (Bool (Set (Const "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Const "p1")) "," (Set (Const "p2")) "," (Set (Const "p3")) ")" ))  ")" )
 ; func  :::"tricord2":::  "(" "p1" "," "p2" "," "p3" "," "p" ")"  ->   ($#m1_subset_1 :::"Real":::) means :: EUCLID_3:def 12 (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  it ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool "p"  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  "p1" ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" it  ($#k1_rlvect_1 :::"*"::: )  "p2" ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  "p3" ")" )))  ")" )); end; 










:: deftheorem    defines :::"tricord2"::: EUCLID_3:def 12 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Set (Var "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1"))) "," (Set (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  ) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ))) "holds"  (Bool  "for" (Set (Var "b6")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_euclid_3 :::"tricord2"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )) "iff" (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b6")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b6"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p3")) ")" )))  ")" ))  ")" )))); 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "p1", "p2", "p3", "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); assume 
(Bool  "("  (Bool (Set (Set (Const "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Const "p1"))) "," (Set (Set (Const "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Const "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  ) & (Bool (Set (Const "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Const "p1")) "," (Set (Const "p2")) "," (Set (Const "p3")) ")" ))  ")" )
 ; func  :::"tricord3":::  "(" "p1" "," "p2" "," "p3" "," "p" ")"  ->   ($#m1_subset_1 :::"Real":::) means :: EUCLID_3:def 13 (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  it)  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool "p"  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  "p1" ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  "p2" ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" it  ($#k1_rlvect_1 :::"*"::: )  "p3" ")" )))  ")" )); end; 










:: deftheorem    defines :::"tricord3"::: EUCLID_3:def 13 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Set (Var "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1"))) "," (Set (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  ) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_euclid_3 :::"plane"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ))) "holds"  (Bool  "for" (Set (Var "b6")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_euclid_3 :::"tricord3"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )) "iff" (Bool  "ex" (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "b6")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a1"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b6"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p3")) ")" )))  ")" ))  ")" )))); 
 definitionlet "p1", "p2", "p3" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); func  :::"trcmap1":::  "(" "p1" "," "p2" "," "p3" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) means :: EUCLID_3:def 14 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_euclid_3 :::"tricord1"::: )   "(" "p1" "," "p2" "," "p3" "," (Set (Var "p")) ")" ))); end; 







:: deftheorem    defines :::"trcmap1"::: EUCLID_3:def 14 :  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k13_euclid_3 :::"trcmap1"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set (Var "b4"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_euclid_3 :::"tricord1"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )))  ")" ))); 
 definitionlet "p1", "p2", "p3" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); func  :::"trcmap2":::  "(" "p1" "," "p2" "," "p3" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) means :: EUCLID_3:def 15 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_euclid_3 :::"tricord2"::: )   "(" "p1" "," "p2" "," "p3" "," (Set (Var "p")) ")" ))); end; 







:: deftheorem    defines :::"trcmap2"::: EUCLID_3:def 15 :  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k14_euclid_3 :::"trcmap2"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set (Var "b4"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_euclid_3 :::"tricord2"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )))  ")" ))); 
 definitionlet "p1", "p2", "p3" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); func  :::"trcmap3":::  "(" "p1" "," "p2" "," "p3" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) means :: EUCLID_3:def 16 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_euclid_3 :::"tricord3"::: )   "(" "p1" "," "p2" "," "p3" "," (Set (Var "p")) ")" ))); end; 







:: deftheorem    defines :::"trcmap3"::: EUCLID_3:def 16 :  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_euclid_3 :::"trcmap3"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set (Var "b4"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_euclid_3 :::"tricord3"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )))  ")" ))); 
 
theorem :: EUCLID_3:55 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Set (Var "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1"))) "," (Set (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_euclid_3 :::"outside_of_triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k10_euclid_3 :::"tricord1"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set   ($#k11_euclid_3 :::"tricord2"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set   ($#k12_euclid_3 :::"tricord3"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) ; 
 
theorem :: EUCLID_3:56 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Set (Var "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1"))) "," (Set (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_euclid_3 :::"Triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k10_euclid_3 :::"tricord1"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k11_euclid_3 :::"tricord2"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k12_euclid_3 :::"tricord3"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("  (Bool (Set   ($#k10_euclid_3 :::"tricord1"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set   ($#k11_euclid_3 :::"tricord2"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set   ($#k12_euclid_3 :::"tricord3"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )  ")" )) ; 
 
theorem :: EUCLID_3:57 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Set (Var "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1"))) "," (Set (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_euclid_3 :::"Triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )) "iff" (Bool  "("  (Bool  "("  (Bool (Set   ($#k10_euclid_3 :::"tricord1"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k11_euclid_3 :::"tricord2"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k12_euclid_3 :::"tricord3"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set   ($#k10_euclid_3 :::"tricord1"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k11_euclid_3 :::"tricord2"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k12_euclid_3 :::"tricord3"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set   ($#k10_euclid_3 :::"tricord1"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k11_euclid_3 :::"tricord2"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k12_euclid_3 :::"tricord3"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )  ")" )) ; 
 
theorem :: EUCLID_3:58 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Set (Var "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1"))) "," (Set (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_euclid_3 :::"inside_of_triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k10_euclid_3 :::"tricord1"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k11_euclid_3 :::"tricord2"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k12_euclid_3 :::"tricord3"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) ; 
 
theorem :: EUCLID_3:59 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Set (Var "p2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1"))) "," (Set (Set (Var "p3"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p1")))  ($#r1_euclid_3 :::"are_lindependent2"::: )  )) "holds"  (Bool  "not" (Bool (Set   ($#k7_euclid_3 :::"inside_of_triangle"::: )   "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) ;