:: MENELAUS semantic presentation begin notationlet "X", "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); synonym "X" :::"is_parallel_to"::: "Y" for "X" :::"misses"::: "Y"; end; definitionlet "X", "Y", "Z" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); pred "X" "," "Y" "," "Z" :::"are_concurrent"::: means :: MENELAUS:def 1 (Bool "(" (Bool "(" (Bool "X" ($#r1_xboole_0 :::"is_parallel_to"::: ) "Y") & (Bool "Y" ($#r1_xboole_0 :::"is_parallel_to"::: ) "Z") & (Bool "Z" ($#r1_xboole_0 :::"is_parallel_to"::: ) "X") ")" ) "or" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "Y") & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "Z") ")" )) ")" ); end; :: deftheorem defines :::"are_concurrent"::: MENELAUS:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ($#r1_menelaus :::"are_concurrent"::: ) ) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "X")) ($#r1_xboole_0 :::"is_parallel_to"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r1_xboole_0 :::"is_parallel_to"::: ) (Set (Var "Z"))) & (Bool (Set (Var "Z")) ($#r1_xboole_0 :::"is_parallel_to"::: ) (Set (Var "X"))) ")" ) "or" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "Z"))) ")" )) ")" ) ")" )); theorem :: MENELAUS:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "B")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k17_euclid :::"`1"::: ) ")" ))) & (Bool (Set (Set "(" (Set (Var "A")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "B")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k18_euclid :::"`2"::: ) ")" ))) ")" )) ; theorem :: MENELAUS:2 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k17_euclid :::"`1"::: ) ")" ))) & (Bool (Set (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k18_euclid :::"`2"::: ) ")" ))) ")" ))) ; theorem :: MENELAUS:3 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "A")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "A")) ($#k17_euclid :::"`1"::: ) ")" ))) & (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "A")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "A")) ($#k18_euclid :::"`2"::: ) ")" ))) ")" )) ; theorem :: MENELAUS:4 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "," (Set (Var "mu")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ))) ")" ))) ; theorem :: MENELAUS:5 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ))) ")" ))) ; theorem :: MENELAUS:6 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "," (Set (Var "mu")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "mu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "mu")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "mu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "mu")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ))) ")" ))) ; theorem :: MENELAUS:7 (Bool "for" (Set (Var "A")) "," (Set (Var "A1")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A1")) ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "A1")) "," (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" ))))) ; theorem :: MENELAUS:8 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Bool "not" (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )))) "holds" (Bool (Set ($#k4_euclid_3 :::"angle"::: ) "(" (Set (Var "B")) "," (Set (Var "A")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ; theorem :: MENELAUS:9 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_euclid_6 :::"is_collinear"::: ) ) "iff" (Bool (Set ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: MENELAUS:10 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "B")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "C")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "C")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2)))) ; theorem :: MENELAUS:11 (Bool "for" (Set (Var "A")) "," (Set (Var "A1")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "A1")) ")" ) "," (Set (Var "B")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "A1")) "," (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" ) "," (Set (Var "B")) "," (Set (Var "C")) ")" ")" )))) ; theorem :: MENELAUS:12 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ))) "holds" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ))) ; theorem :: MENELAUS:13 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set (Var "C")))) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_euclid_6 :::"is_collinear"::: ) ) "iff" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" )) ")" )) ; theorem :: MENELAUS:14 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" )))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "A1"))))) ; theorem :: MENELAUS:15 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_euclid_6 :::"is_a_triangle"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "A")) "," (Set (Var "C")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "A")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) ")" )) ; theorem :: MENELAUS:16 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "," (Set (Var "mu")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Var "mu")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set (Var "mu")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "not" (Bool (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "A1")) ")" ) ($#r1_xboole_0 :::"is_parallel_to"::: ) (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "B1")) ")" ))) ")" ))) ; begin theorem :: MENELAUS:17 (Bool "for" (Set (Var "A1")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "B1")) "," (Set (Var "A")) "," (Set (Var "C1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "," (Set (Var "mu")) "," (Set (Var "nu")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "nu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" )))) "holds" (Bool (Set ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "C1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set (Var "mu")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "nu")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" ")" ))))) ; theorem :: MENELAUS:18 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "C1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "," (Set (Var "mu")) "," (Set (Var "nu")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "nu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ))) & (Bool (Set (Var "lambda")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "mu")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "nu")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "C1")) ($#r1_euclid_6 :::"is_collinear"::: ) ) "iff" (Bool (Set (Set "(" (Set "(" (Set (Var "lambda")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "mu")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "nu")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k19_binop_2 :::"-"::: ) (Num 1))) ")" ))) ; theorem :: MENELAUS:19 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "A2")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "," (Set (Var "mu")) "," (Set (Var "nu")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "nu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ))) & (Bool (Set (Var "lambda")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "mu")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "nu")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "A")) "," (Set (Var "A1")) "," (Set (Var "C2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "B1")) "," (Set (Var "C2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "B1")) "," (Set (Var "A2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "C")) "," (Set (Var "C1")) "," (Set (Var "A2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "A")) "," (Set (Var "A1")) "," (Set (Var "B2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "C")) "," (Set (Var "C1")) "," (Set (Var "B2")) ($#r1_euclid_6 :::"is_collinear"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set (Var "mu")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "nu")) ($#k11_binop_2 :::"*"::: ) (Set (Var "lambda")) ")" ) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k11_binop_2 :::"*"::: ) (Set (Var "nu")) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) "," (Set (Var "C2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "mu")) ($#k11_binop_2 :::"*"::: ) (Set (Var "nu")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "lambda")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set (Var "mu")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "nu")) ($#k11_binop_2 :::"*"::: ) (Set (Var "lambda")) ")" ) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k11_binop_2 :::"*"::: ) (Set (Var "nu")) ")" ) ")" ) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" ")" ))) ")" ))) ; theorem :: MENELAUS:20 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "A2")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k18_binop_2 :::"/"::: ) (Num 3) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 3) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k18_binop_2 :::"/"::: ) (Num 3) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 3) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k18_binop_2 :::"/"::: ) (Num 3) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 3) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ))) & (Bool (Set (Var "A")) "," (Set (Var "A1")) "," (Set (Var "C2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "B1")) "," (Set (Var "C2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "B1")) "," (Set (Var "A2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "C")) "," (Set (Var "C1")) "," (Set (Var "A2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "A")) "," (Set (Var "A1")) "," (Set (Var "B2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "C")) "," (Set (Var "C1")) "," (Set (Var "B2")) ($#r1_euclid_6 :::"is_collinear"::: ) )) "holds" (Bool (Set ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) "," (Set (Var "C2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_euclid_6 :::"the_area_of_polygon3"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ($#k12_binop_2 :::"/"::: ) (Num 7)))) ; theorem :: MENELAUS:21 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "C1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "," (Set (Var "mu")) "," (Set (Var "nu")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "nu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ))) & (Bool (Set (Var "lambda")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "mu")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "nu")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k11_binop_2 :::"*"::: ) (Set (Var "mu")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "nu")) ($#k11_binop_2 :::"*"::: ) (Set (Var "lambda")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k11_binop_2 :::"*"::: ) (Set (Var "nu")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "lambda")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "mu")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "nu")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "ex" (Set (Var "A2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "B1")) "," (Set (Var "A2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) & (Bool (Set (Var "C")) "," (Set (Var "C1")) "," (Set (Var "A2")) ($#r1_euclid_6 :::"is_collinear"::: ) ) ")" )) ")" ))) ; theorem :: MENELAUS:22 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "C1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "lambda")) "," (Set (Var "mu")) "," (Set (Var "nu")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#r1_euclid_6 :::"is_a_triangle"::: ) ) & (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "lambda")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "C")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "mu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "nu")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "B")) ")" ))) & (Bool (Set (Var "lambda")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "mu")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "nu")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "lambda")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "lambda")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "mu")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "mu")) ")" ) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "nu")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "nu")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "A1")) ")" ) "," (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "B1")) ")" ) "," (Set ($#k4_euclid_4 :::"Line"::: ) "(" (Set (Var "C")) "," (Set (Var "C1")) ")" ) ($#r1_menelaus :::"are_concurrent"::: ) ) ")" ))) ;