:: EUCLID_5  semantic presentation begin  












theorem :: EUCLID_5:1 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) )))) ; 
 definitionlet "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ); func "p" :::"`1":::  ->   ($#m1_subset_1 :::"Real":::) equals :: EUCLID_5:def 1 (Set "p"  ($#k1_seq_1 :::"."::: )  (Num 1)); func "p" :::"`2":::  ->   ($#m1_subset_1 :::"Real":::) equals :: EUCLID_5:def 2 (Set "p"  ($#k1_seq_1 :::"."::: )  (Num 2)); func "p" :::"`3":::  ->   ($#m1_subset_1 :::"Real":::) equals :: EUCLID_5:def 3 (Set "p"  ($#k1_seq_1 :::"."::: )  (Num 3)); end; 















:: deftheorem    defines :::"`1"::: EUCLID_5:def 1 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_euclid_5 :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Num 1)))); 
 
:: deftheorem    defines :::"`2"::: EUCLID_5:def 2 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set (Var "p"))  ($#k2_euclid_5 :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Num 2)))); 
 
:: deftheorem    defines :::"`3"::: EUCLID_5:def 3 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set (Var "p"))  ($#k3_euclid_5 :::"`3"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Num 3)))); 
 notationlet "x", "y", "z" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; synonym :::"|[":::"x" "," "y" "," "z":::"]|"::: for :::"<*":::"x" "," "y" "," "z":::"*>":::; end; definitionlet "x", "y", "z" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"|["::: redefine func :::"|[":::"x" "," "y" "," "z":::"]|"::: ->   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ); end; 
theorem :: EUCLID_5:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k4_euclid_5 :::"]|"::: ) )  ($#k1_euclid_5 :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k4_euclid_5 :::"]|"::: ) )  ($#k2_euclid_5 :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k4_euclid_5 :::"]|"::: ) )  ($#k3_euclid_5 :::"`3"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "z")))  ")" )) ; 
 
theorem :: EUCLID_5:3 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "(" (Set (Var "p"))  ($#k1_euclid_5 :::"`1"::: )  ")" ) "," (Set  "(" (Set (Var "p"))  ($#k2_euclid_5 :::"`2"::: )  ")" ) "," (Set  "(" (Set (Var "p"))  ($#k3_euclid_5 :::"`3"::: )  ")" ) ($#k4_euclid_5 :::"]|"::: ) ))) ; 
 
theorem :: EUCLID_5:4 (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) )) ; 
 














theorem :: EUCLID_5:5 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set (Var "p1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p2")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k1_euclid_5 :::"`1"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "p2"))  ($#k1_euclid_5 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k2_euclid_5 :::"`2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "p2"))  ($#k2_euclid_5 :::"`2"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k3_euclid_5 :::"`3"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "p2"))  ($#k3_euclid_5 :::"`3"::: )  ")" ) ")" ) ($#k4_euclid_5 :::"]|"::: ) ))) ; 
 
theorem :: EUCLID_5:6 (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) ($#k4_euclid_5 :::"]|"::: ) )  ($#k3_rlvect_1 :::"+"::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) ($#k4_euclid_5 :::"]|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "(" (Set (Var "x1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x2")) ")" ) "," (Set  "(" (Set (Var "y1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "y2")) ")" ) "," (Set  "(" (Set (Var "z1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "z2")) ")" ) ($#k4_euclid_5 :::"]|"::: ) ))) ; 
 
theorem :: EUCLID_5:7 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k1_euclid_5 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k2_euclid_5 :::"`2"::: )  ")" ) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k3_euclid_5 :::"`3"::: )  ")" ) ")" ) ($#k4_euclid_5 :::"]|"::: ) )))) ; 
 
theorem :: EUCLID_5:8 (Bool  "for" (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_rlvect_1 :::"*"::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) ($#k4_euclid_5 :::"]|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x1")) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "y1")) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "z1")) ")" ) ($#k4_euclid_5 :::"]|"::: ) ))) ; 
 
theorem :: EUCLID_5:9 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")) ")" )  ($#k1_euclid_5 :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k1_euclid_5 :::"`1"::: )  ")" ))) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")) ")" )  ($#k2_euclid_5 :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k2_euclid_5 :::"`2"::: )  ")" ))) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")) ")" )  ($#k3_euclid_5 :::"`3"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k3_euclid_5 :::"`3"::: )  ")" )))  ")" ))) ; 
 
theorem :: EUCLID_5:10 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set   ($#k4_algstr_0 :::"-"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k1_euclid_5 :::"`1"::: )  ")" ) ")" ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k2_euclid_5 :::"`2"::: )  ")" ) ")" ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k3_euclid_5 :::"`3"::: )  ")" ) ")" ) ($#k4_euclid_5 :::"]|"::: ) ))) ; 
 
theorem :: EUCLID_5:11 (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k4_algstr_0 :::"-"::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) ($#k4_euclid_5 :::"]|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "x1")) ")" ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "y1")) ")" ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "z1")) ")" ) ($#k4_euclid_5 :::"]|"::: ) ))) ; 
 
theorem :: EUCLID_5:12 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set (Var "p1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k1_euclid_5 :::"`1"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "p2"))  ($#k1_euclid_5 :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k2_euclid_5 :::"`2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "p2"))  ($#k2_euclid_5 :::"`2"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k3_euclid_5 :::"`3"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "p2"))  ($#k3_euclid_5 :::"`3"::: )  ")" ) ")" ) ($#k4_euclid_5 :::"]|"::: ) ))) ; 
 
theorem :: EUCLID_5:13 (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) ($#k4_euclid_5 :::"]|"::: ) )  ($#k5_algstr_0 :::"-"::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) ($#k4_euclid_5 :::"]|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "(" (Set (Var "x1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x2")) ")" ) "," (Set  "(" (Set (Var "y1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "y2")) ")" ) "," (Set  "(" (Set (Var "z1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "z2")) ")" ) ($#k4_euclid_5 :::"]|"::: ) ))) ; 
 definitionlet "p1", "p2" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ); func "p1" :::"<X>"::: "p2" ->   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) equals :: EUCLID_5:def 4 (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "(" (Set  "(" (Set  "(" "p1"  ($#k2_euclid_5 :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "p2"  ($#k3_euclid_5 :::"`3"::: )  ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" "p1"  ($#k3_euclid_5 :::"`3"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "p2"  ($#k2_euclid_5 :::"`2"::: )  ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" "p1"  ($#k3_euclid_5 :::"`3"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "p2"  ($#k1_euclid_5 :::"`1"::: )  ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" "p1"  ($#k1_euclid_5 :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "p2"  ($#k3_euclid_5 :::"`3"::: )  ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" "p1"  ($#k1_euclid_5 :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "p2"  ($#k2_euclid_5 :::"`2"::: )  ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" "p1"  ($#k2_euclid_5 :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "p2"  ($#k1_euclid_5 :::"`1"::: )  ")" ) ")" ) ")" ) ($#k4_euclid_5 :::"]|"::: ) ); end; 






:: deftheorem    defines :::"<X>"::: EUCLID_5:def 4 :  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p2")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "(" (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k2_euclid_5 :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k3_euclid_5 :::"`3"::: )  ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k3_euclid_5 :::"`3"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k2_euclid_5 :::"`2"::: )  ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k3_euclid_5 :::"`3"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k1_euclid_5 :::"`1"::: )  ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k1_euclid_5 :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k3_euclid_5 :::"`3"::: )  ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k1_euclid_5 :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k2_euclid_5 :::"`2"::: )  ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k2_euclid_5 :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k1_euclid_5 :::"`1"::: )  ")" ) ")" ) ")" ) ($#k4_euclid_5 :::"]|"::: ) ))); 
 
theorem :: EUCLID_5:14 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k4_euclid_5 :::"]|"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k1_euclid_5 :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set (Var "p"))  ($#k2_euclid_5 :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set (Set (Var "p"))  ($#k3_euclid_5 :::"`3"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "z")))  ")" ))) ; 
 
theorem :: EUCLID_5:15 (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) ($#k4_euclid_5 :::"]|"::: ) )  ($#k5_euclid_5 :::"<X>"::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) ($#k4_euclid_5 :::"]|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "y1"))  ($#k8_real_1 :::"*"::: )  (Set (Var "z2")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "z1"))  ($#k8_real_1 :::"*"::: )  (Set (Var "y2")) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "z1"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x2")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "x1"))  ($#k8_real_1 :::"*"::: )  (Set (Var "z2")) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k8_real_1 :::"*"::: )  (Set (Var "y2")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "y1"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x2")) ")" ) ")" ) ($#k4_euclid_5 :::"]|"::: ) ))) ; 
 
theorem :: EUCLID_5:16 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p2")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p1")) ")" )  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set  "(" (Set (Var "x"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" )))  ")" ))) ; 
 
theorem :: EUCLID_5:17 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p2")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "p2"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p1")) ")" )))) ; 
 
theorem :: EUCLID_5:18 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "p1")) ")" )  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" )))) ; 
 
theorem :: EUCLID_5:19 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  ($#k4_euclid_5 :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) )  ($#k5_euclid_5 :::"<X>"::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k4_euclid_5 :::"]|"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" )))) ; 
 
theorem :: EUCLID_5:20 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x1")) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) )  ($#k5_euclid_5 :::"<X>"::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x2")) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" )))) ; 
 
theorem :: EUCLID_5:21 (Bool  "for" (Set (Var "y1")) "," (Set (Var "y2")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  ($#k4_euclid_5 :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y1")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) )  ($#k5_euclid_5 :::"<X>"::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y2")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" )))) ; 
 
theorem :: EUCLID_5:22 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  ($#k4_euclid_5 :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z1")) ($#k4_euclid_5 :::"]|"::: ) )  ($#k5_euclid_5 :::"<X>"::: )  (Set  ($#k4_euclid_5 :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z2")) ($#k4_euclid_5 :::"]|"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" )))) ; 
 
theorem :: EUCLID_5:23 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set  "(" (Set (Var "p2"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p2")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p3")) ")" )))) ; 
 
theorem :: EUCLID_5:24 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set  "(" (Set (Var "p1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p2")) ")" )  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p3")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p3")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "p2"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p3")) ")" )))) ; 
 
theorem :: EUCLID_5:25 (Bool  "for" (Set (Var "p1")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" )))) ; 
 
theorem :: EUCLID_5:26 (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 3) ")" ) "holds"  (Bool (Set (Set  "(" (Set (Var "p1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p2")) ")" )  ($#k5_euclid_5 :::"<X>"::: )  (Set  "(" (Set (Var "p3"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p4")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p3")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p4")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "p2"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p3")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "p2"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p4")) ")" )))) ; 
 
theorem :: EUCLID_5:27 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_finseq_4 :::"<*"::: ) (Set  "(" (Set (Var "p"))  ($#k1_euclid_5 :::"`1"::: )  ")" ) "," (Set  "(" (Set (Var "p"))  ($#k2_euclid_5 :::"`2"::: )  ")" ) "," (Set  "(" (Set (Var "p"))  ($#k3_euclid_5 :::"`3"::: )  ")" ) ($#k3_finseq_4 :::"*>"::: ) ))) ; 
 
theorem :: EUCLID_5:28 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))  ($#r1_hidden :::"="::: )  (Num 3)) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2")))  ($#r1_hidden :::"="::: )  (Num 3))) "holds"  (Bool (Set   ($#k14_rvsum_1 :::"mlt"::: )   "(" (Set (Var "f1")) "," (Set (Var "f2")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k3_finseq_4 :::"<*"::: ) (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Num 1) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k1_seq_1 :::"."::: )  (Num 3) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_seq_1 :::"."::: )  (Num 3) ")" ) ")" ) ($#k3_finseq_4 :::"*>"::: ) ))) ; 
 
theorem :: EUCLID_5:29 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k1_euclid_5 :::"`1"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k1_euclid_5 :::"`1"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k2_euclid_5 :::"`2"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k2_euclid_5 :::"`2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p1"))  ($#k3_euclid_5 :::"`3"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p2"))  ($#k3_euclid_5 :::"`3"::: )  ")" ) ")" )))) ; 
 
theorem :: EUCLID_5:30 (Bool  "for" (Set (Var "x3")) "," (Set (Var "y3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set  ($#k23_rvsum_1 :::"|("::: ) (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_euclid_5 :::"]|"::: ) ) "," (Set  ($#k4_euclid_5 :::"|["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k4_euclid_5 :::"]|"::: ) ) ($#k23_rvsum_1 :::")|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k8_real_1 :::"*"::: )  (Set (Var "y1")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "x2"))  ($#k8_real_1 :::"*"::: )  (Set (Var "y2")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "x3"))  ($#k8_real_1 :::"*"::: )  (Set (Var "y3")) ")" ))))) ; 
 definitionlet "p1", "p2", "p3" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ); func :::"|{":::"p1" "," "p2" "," "p3":::"}|"::: ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   equals :: EUCLID_5:def 5 (Set  ($#k23_rvsum_1 :::"|("::: ) "p1" "," (Set  "(" "p2"  ($#k5_euclid_5 :::"<X>"::: )  "p3" ")" ) ($#k23_rvsum_1 :::")|"::: ) ); end; 







:: deftheorem    defines :::"|{"::: EUCLID_5:def 5 :  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set  ($#k6_euclid_5 :::"|{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k6_euclid_5 :::"}|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set  "(" (Set (Var "p2"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p3")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ))); 
 
theorem :: EUCLID_5:31 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"   (Bool  "("  (Bool (Set  ($#k6_euclid_5 :::"|{"::: ) (Set (Var "p1")) "," (Set (Var "p1")) "," (Set (Var "p2")) ($#k6_euclid_5 :::"}|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set  ($#k6_euclid_5 :::"|{"::: ) (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "p2")) ($#k6_euclid_5 :::"}|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: EUCLID_5:32 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set  "(" (Set (Var "p2"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p2")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p3")) ")" )))) ; 
 
theorem :: EUCLID_5:33 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set  ($#k6_euclid_5 :::"|{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k6_euclid_5 :::"}|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k6_euclid_5 :::"|{"::: ) (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p1")) ($#k6_euclid_5 :::"}|"::: ) ))) ; 
 
theorem :: EUCLID_5:34 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set  ($#k6_euclid_5 :::"|{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k6_euclid_5 :::"}|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k6_euclid_5 :::"|{"::: ) (Set (Var "p3")) "," (Set (Var "p1")) "," (Set (Var "p2")) ($#k6_euclid_5 :::"}|"::: ) ))) ; 
 
theorem :: EUCLID_5:35 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 3) ")" ) "holds"  (Bool (Set  ($#k6_euclid_5 :::"|{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k6_euclid_5 :::"}|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k23_rvsum_1 :::"|("::: ) (Set  "(" (Set (Var "p1"))  ($#k5_euclid_5 :::"<X>"::: )  (Set (Var "p2")) ")" ) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ))) ;