:: EUCLID_6 semantic presentation begin theorem :: EUCLID_6:1 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) ")" ")" ))) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) ")" ")" )))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) ")" ))) ; theorem :: EUCLID_6:2 (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 ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" ")" ) ")" )))) ; theorem :: EUCLID_6:3 (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 ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" ")" )))) ; theorem :: EUCLID_6:4 (Bool "for" (Set (Var "p1")) "," (Set (Var "p4")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p4")) "," (Set (Var "p2")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p2")) "," (Set (Var "p4")) "," (Set (Var "p3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p4")) "," (Set (Var "p3")) ")" )) "or" (Bool (Set (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p4")) "," (Set (Var "p2")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p2")) "," (Set (Var "p4")) "," (Set (Var "p3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p4")) "," (Set (Var "p3")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ))) ")" )) ; definitionlet "p1", "p2", "p3" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func :::"the_area_of_polygon3"::: "(" "p1" "," "p2" "," "p3" ")" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: EUCLID_6:def 1 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "p1" ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" "p2" ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" "p2" ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" "p1" ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" "p2" ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" "p3" ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" "p3" ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" "p2" ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" "p3" ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" "p1" ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" "p1" ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" "p3" ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)); end; :: deftheorem defines :::"the_area_of_polygon3"::: EUCLID_6:def 1 : (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 ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p3")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "p3")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p3")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p3")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))); definitionlet "p1", "p2", "p3" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func :::"the_perimeter_of_polygon3"::: "(" "p1" "," "p2" "," "p3" ")" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: EUCLID_6:def 2 (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" "p2" ($#k5_algstr_0 :::"-"::: ) "p1" ")" ) ($#k12_euclid :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" "p3" ($#k5_algstr_0 :::"-"::: ) "p2" ")" ) ($#k12_euclid :::".|"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" "p1" ($#k5_algstr_0 :::"-"::: ) "p3" ")" ) ($#k12_euclid :::".|"::: ) )); end; :: deftheorem defines :::"the_perimeter_of_polygon3"::: EUCLID_6:def 2 : (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 ($#k2_euclid_6 :::"the_perimeter_of_polygon3"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) )))); theorem :: EUCLID_6:5 (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 ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: EUCLID_6:6 (Bool "for" (Set (Var "p2")) "," (Set (Var "p1")) "," (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")))) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "p3")) ")" ")" ) ")" )))) ; theorem :: EUCLID_6:7 (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 "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ))) "holds" (Bool (Set (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k5_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ")" ) ")" ) ")" ))))) ; begin theorem :: EUCLID_6:8 (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ; theorem :: EUCLID_6:9 (Bool "for" (Set (Var "p")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p2")) "," (Set (Var "p3")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p")) "," (Set (Var "p2")) "," (Set (Var "p1")) ")" ))) ; theorem :: EUCLID_6:10 (Bool "for" (Set (Var "p")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p2")) "," (Set (Var "p3")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p")) ")" ))) ; theorem :: EUCLID_6:11 (Bool "for" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p2")) "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 "p")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))) ; theorem :: EUCLID_6:12 (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p4")) ")" )) & (Bool (Set (Var "p3")) ($#r1_hidden :::"<>"::: ) (Set (Var "p4"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))) & (Bool (Bool "not" (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p4")) ")" )))) "holds" (Bool (Set (Var "p4")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) ")" ))) ; theorem :: EUCLID_6:13 (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Bool "not" (Set (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p2")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p2")) "," (Set (Var "p")) "," (Set (Var "p3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )))) "holds" (Bool (Set (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p2")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p2")) "," (Set (Var "p")) "," (Set (Var "p3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )))) ; theorem :: EUCLID_6:14 (Bool "for" (Set (Var "p")) "," (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 "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool "(" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2))) "or" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" )) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p")) "," (Set (Var "p2")) ")" ))) ; theorem :: EUCLID_6:15 (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p2")) "," (Set (Var "p4")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p4")))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p")) "," (Set (Var "p4")) ")" ))) ; theorem :: EUCLID_6:16 (Bool "for" (Set (Var "p3")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) )) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ))) ; theorem :: EUCLID_6:17 (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 (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool "(" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: EUCLID_6:18 (Bool "for" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))) & (Bool "(" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2))) "or" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" )) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ))) ; theorem :: EUCLID_6:19 (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 ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3")))) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ))) "implies" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) )) ")" & "(" (Bool (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ))) "implies" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" )) ")" ")" )) ; definitionlet "p1", "p2", "p3" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); pred "p1" "," "p2" "," "p3" :::"is_collinear"::: means :: EUCLID_6:def 3 (Bool "(" (Bool "p1" ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" "p2" "," "p3" ")" )) "or" (Bool "p2" ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" "p3" "," "p1" ")" )) "or" (Bool "p3" ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" "p1" "," "p2" ")" )) ")" ); end; :: deftheorem defines :::"is_collinear"::: EUCLID_6:def 3 : (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 "(" (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#r1_euclid_6 :::"is_collinear"::: ) ) "iff" (Bool "(" (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p2")) "," (Set (Var "p3")) ")" )) "or" (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p3")) "," (Set (Var "p1")) ")" )) "or" (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) ")" ) ")" )); notationlet "p1", "p2", "p3" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); antonym "p1" "," "p2" "," "p3" :::"is_a_triangle"::: for "p1" "," "p2" "," "p3" :::"is_collinear"::: ; end; theorem :: EUCLID_6:20 (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 "(" (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) "iff" (Bool "(" (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ")" ) ")" )) ; theorem :: EUCLID_6:21 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) ")" )) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p6")) "," (Set (Var "p4")) "," (Set (Var "p5")) ")" ))) "holds" (Bool "(" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p4")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p6")) ")" ) ($#k12_euclid :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p6")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p5")) ")" ) ($#k12_euclid :::".|"::: ) ))) & (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p5")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p4")) ")" ) ($#k12_euclid :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p6")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p5")) ")" ) ($#k12_euclid :::".|"::: ) ))) & (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p5")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p4")) ")" ) ($#k12_euclid :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p4")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p6")) ")" ) ($#k12_euclid :::".|"::: ) ))) ")" )) ; theorem :: EUCLID_6:22 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) ")" )) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p5")) "," (Set (Var "p6")) "," (Set (Var "p4")) ")" ))) "holds" (Bool "(" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p4")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p6")) ")" ) ($#k12_euclid :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p5")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p4")) ")" ) ($#k12_euclid :::".|"::: ) ))) & (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p6")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p5")) ")" ) ($#k12_euclid :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p5")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p4")) ")" ) ($#k12_euclid :::".|"::: ) ))) & (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p6")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p5")) ")" ) ($#k12_euclid :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p4")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p6")) ")" ) ($#k12_euclid :::".|"::: ) ))) ")" )) ; theorem :: EUCLID_6:23 (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")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p1")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ")" )) ; theorem :: EUCLID_6:24 (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")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p1")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p3")) "," (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ")" )) ; theorem :: EUCLID_6:25 (Bool "for" (Set (Var "p")) "," (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 "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1")))) ; theorem :: EUCLID_6:26 (Bool "for" (Set (Var "p")) "," (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 "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Bool "not" (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ))) ; theorem :: EUCLID_6:27 (Bool "for" (Set (Var "p")) "," (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 "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Bool "not" (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ))) ; theorem :: EUCLID_6:28 (Bool "for" (Set (Var "p")) "," (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 "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Bool "not" (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )))) "holds" (Bool "ex" (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "p4")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" )) ")" ))) ; theorem :: EUCLID_6:29 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k8_jgraph_6 :::"outside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ")" )))))) ; theorem :: EUCLID_6:30 (Bool "for" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p4")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p4")) ")" )) & (Bool (Set (Var "p3")) ($#r1_hidden :::"<>"::: ) (Set (Var "p4")))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))))) ; theorem :: EUCLID_6:31 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p")) "," (Set (Var "pc")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "pc")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Var "pc")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool (Bool "not" (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "pc")) "," (Set (Var "p2")) ")" )))) "holds" (Bool (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p2")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "pc")) "," (Set (Var "p2")) ")" )))) ; theorem :: EUCLID_6:32 (Bool "for" (Set (Var "p1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (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 (Var "p2"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) ")" )))) ; theorem :: EUCLID_6:33 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p")) "," (Set (Var "pc")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "pc")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool (Bool "not" (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "pc")) "," (Set (Var "p2")) ")" )))) "holds" (Bool (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p2")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "pc")) "," (Set (Var "p2")) ")" )))) ; theorem :: EUCLID_6:34 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p4")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p4"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "p4"))) & (Bool (Bool "not" (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p4")) "," (Set (Var "p2")) ")" ))) & (Bool (Bool "not" (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p4")) "," (Set (Var "p2")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p4")) "," (Set (Var "p2")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))))) ; theorem :: EUCLID_6: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) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3")))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )))) ; theorem :: EUCLID_6:36 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p4")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p2")) "," (Set (Var "p4")) ")" )) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p4")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ")" )))) ; theorem :: EUCLID_6: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) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3")))) "holds" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p3"))))) ; theorem :: EUCLID_6:38 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p4")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p2")) "," (Set (Var "p4")) ")" ))) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p4")) ")" ) ($#k12_euclid :::".|"::: ) ))))) ; begin theorem :: EUCLID_6:39 (Bool "for" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) )) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_euclid_6 :::"the_perimeter_of_polygon3"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ")" ) ($#k6_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "s")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ")" ))))) ; theorem :: EUCLID_6:40 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p4")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p3")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p2")) "," (Set (Var "p4")) ")" ))) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p4")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p4")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p3")) ")" ) ($#k12_euclid :::".|"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p4")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ) ")" ))))) ; begin theorem :: EUCLID_6:41 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ))) & (Bool (Set (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ))) ")" )) ; theorem :: EUCLID_6:42 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" )) ; theorem :: EUCLID_6:43 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k12_euclid :::".|"::: ) ))) ; theorem :: EUCLID_6:44 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Bool "not" (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ))))) ; theorem :: EUCLID_6:45 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Bool "not" (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ))))) ; theorem :: EUCLID_6:46 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Bool "not" (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) ")" ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ))))) ; theorem :: EUCLID_6:47 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Bool "not" (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p4")) "," (Set (Var "p5")) "," (Set (Var "p6")) ")" ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 6) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ))))) ; theorem :: EUCLID_6:48 (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 "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_3 :::"euc2cpx"::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ))) & (Bool (Set (Var "c2")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_3 :::"euc2cpx"::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" )))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" )))) ; theorem :: EUCLID_6:49 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "c2")) "," (Set (Var "c3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "c1")) "," (Set (Var "c3")) ")" )) "or" (Bool (Set (Set "(" ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "c2")) "," (Set (Var "c3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "c1")) "," (Set (Var "c3")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ))) ")" )) ; theorem :: EUCLID_6:50 (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 "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_3 :::"euc2cpx"::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ))) & (Bool (Set (Var "c2")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_3 :::"euc2cpx"::: ) (Set "(" (Set (Var "p3")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set "(" (Set (Var "c1")) ($#k1_complex2 :::".|."::: ) (Set (Var "c2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "p3")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "p3")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ")" ))) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" (Set (Var "c1")) ($#k1_complex2 :::".|."::: ) (Set (Var "c2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "p3")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "p3")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ")" ))) & (Bool (Set ($#k17_complex1 :::"|."::: ) (Set (Var "c1")) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "c1")) ($#k17_complex1 :::".|"::: ) )) ")" ))) ; theorem :: EUCLID_6:51 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "q")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q1")) ")" ) ($#k12_euclid :::".|"::: ) )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )))) ; theorem :: EUCLID_6:52 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "q")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q1")) ")" ) ($#k12_euclid :::".|"::: ) )) ")" ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )))) ;