:: EUCLID_4 semantic presentation begin theorem :: EUCLID_4:1 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; theorem :: EUCLID_4:2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))))) ; theorem :: EUCLID_4:3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Num 1) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) ")" ))) ; theorem :: EUCLID_4:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "b")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" )))))) ; theorem :: EUCLID_4:5 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" "not" (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) ")" )))) ; theorem :: EUCLID_4:6 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" )))))) ; theorem :: EUCLID_4:7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" )))))) ; theorem :: EUCLID_4:8 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" "not" (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" )))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x1", "x2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); func :::"Line"::: "(" "x1" "," "x2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) equals :: EUCLID_4:def 1 "{" (Set "(" (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k9_euclid :::"*"::: ) "x1" ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k9_euclid :::"*"::: ) "x2" ")" ) ")" ) where lambda "is" ($#m1_subset_1 :::"Real":::) : (Bool verum) "}" ; end; :: deftheorem defines :::"Line"::: EUCLID_4:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k1_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) where lambda "is" ($#m1_subset_1 :::"Real":::) : (Bool verum) "}" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x1", "x2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); cluster (Set ($#k1_euclid_4 :::"Line"::: ) "(" "x1" "," "x2" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x1", "x2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); :: original: :::"Line"::: redefine func :::"Line"::: "(" "x1" "," "x2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ); commutativity (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))) "holds" (Bool (Set ($#k1_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_4 :::"Line"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) ")" ))) ; end; theorem :: EUCLID_4:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) ")" ))) ; theorem :: EUCLID_4:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "y1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ))) "holds" (Bool (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )))) ; theorem :: EUCLID_4:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "y1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set (Var "y1")) ($#r1_hidden :::"<>"::: ) (Set (Var "y2")))) "holds" (Bool (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); attr "A" is :::"being_line"::: means :: EUCLID_4:def 2 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "st" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) ")" )); end; :: deftheorem defines :::"being_line"::: EUCLID_4:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) ")" )) ")" ))); theorem :: EUCLID_4:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Bool "not" (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "C")))))) ; theorem :: EUCLID_4:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_euclid_4 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) ")" )))) ; theorem :: EUCLID_4:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_euclid_4 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))))) ; theorem :: EUCLID_4:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: EUCLID_4:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) ")" ))) ; theorem :: EUCLID_4:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: EUCLID_4:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" ) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: EUCLID_4:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) "," (Set (Var "x2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k23_rvsum_1 :::")|"::: ) )))))) ; theorem :: EUCLID_4:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k23_rvsum_1 :::")|"::: ) )))))) ; theorem :: EUCLID_4:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set (Var "x2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set "(" ($#k6_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_4:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x1")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_euclid :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k4_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ")" )))))) ; theorem :: EUCLID_4:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set "(" (Set (Var "y1")) ($#k7_euclid :::"+"::: ) (Set (Var "y2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:29 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set "(" (Set (Var "y1")) ($#k8_euclid :::"-"::: ) (Set (Var "y2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:30 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k7_euclid :::"+"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k7_euclid :::"+"::: ) (Set (Var "y2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y1")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:31 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k8_euclid :::"-"::: ) (Set (Var "y2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_real_1 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y1")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:32 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set (Var "y")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "y")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:33 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "y")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "y")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:34 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: EUCLID_4:35 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: EUCLID_4:36 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ; theorem :: EUCLID_4:37 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k8_euclid :::"-"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: EUCLID_4:38 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: EUCLID_4:39 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set (Var "y")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: EUCLID_4:40 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) "{" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "y1")) ($#k8_euclid :::"-"::: ) (Set (Var "x")) ")" ) ($#k12_euclid :::".|"::: ) ) where x "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) "}" )) "holds" (Bool "ex" (Set (Var "y2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_euclid_4 :::"Line"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "y1")) ($#k8_euclid :::"-"::: ) (Set (Var "y2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2"))) "," (Set (Set (Var "y1")) ($#k8_euclid :::"-"::: ) (Set (Var "y2"))) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) ")" ))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p1", "p2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); func :::"Line"::: "(" "p1" "," "p2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) equals :: EUCLID_4:def 3 "{" (Set "(" (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) "p1" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) "p2" ")" ) ")" ) where lambda "is" ($#m1_subset_1 :::"Real":::) : (Bool verum) "}" ; end; :: deftheorem defines :::"Line"::: EUCLID_4:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k3_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")) ")" ) ")" ) where lambda "is" ($#m1_subset_1 :::"Real":::) : (Bool verum) "}" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); let "p1", "p2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k3_euclid_4 :::"Line"::: ) "(" "p1" "," "p2" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p1", "p2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); :: original: :::"Line"::: redefine func :::"Line"::: "(" "p1" "," "p2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); commutativity (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ) "holds" (Bool (Set ($#k3_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_euclid_4 :::"Line"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) ")" ))) ; end; theorem :: EUCLID_4:41 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) ")" ))) ; theorem :: EUCLID_4:42 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "q1")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))) "holds" (Bool (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )))) ; theorem :: EUCLID_4:43 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "q1")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2")))) "holds" (Bool (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" )))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); attr "A" is :::"being_line"::: means :: EUCLID_4:def 4 (Bool "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "st" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) ")" )); end; :: deftheorem defines :::"being_line"::: EUCLID_4:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_euclid_4 :::"being_line"::: ) ) "iff" (Bool "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) ")" )) ")" ))); theorem :: EUCLID_4:44 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "C")) "is" ($#v2_euclid_4 :::"being_line"::: ) ) & (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Bool "not" (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "C")))))) ; theorem :: EUCLID_4:45 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_euclid_4 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) ")" )))) ; theorem :: EUCLID_4:46 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_euclid_4 :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))))) ; theorem :: EUCLID_4:47 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) "{" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "q1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) "}" )) "holds" (Bool "ex" (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "q1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2"))) "," (Set (Set (Var "q1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q2"))) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) ")" ))))) ;