:: MATHMORP semantic presentation begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_algstr_0 :::"addMagma"::: ) ; let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "T")); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "X" :::"+"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: MATHMORP:def 1 "{" (Set "(" (Set (Var "q")) ($#k1_algstr_0 :::"+"::: ) "p" ")" ) where q "is" ($#m1_subset_1 :::"Element":::) "of" "T" : (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "X") "}" ; end; :: deftheorem defines :::"+"::: MATHMORP:def 1 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_algstr_0 :::"addMagma"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "q")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "p")) ")" ) where q "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) : (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" )))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "X" :::"!"::: -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: MATHMORP:def 2 "{" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) where q "is" ($#m1_subset_1 :::"Point":::) "of" "T" : (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "X") "}" ; end; :: deftheorem defines :::"!"::: MATHMORP:def 2 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k2_mathmorp :::"!"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) : (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" ))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_algstr_0 :::"addMagma"::: ) ; let "X", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "X" :::"(-)"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: MATHMORP:def 3 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" "T" : (Bool (Set "B" ($#k1_mathmorp :::"+"::: ) (Set (Var "y"))) ($#r1_tarski :::"c="::: ) "X") "}" ; end; :: deftheorem defines :::"(-)"::: MATHMORP:def 3 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_algstr_0 :::"addMagma"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) : (Bool (Set (Set (Var "B")) ($#k1_mathmorp :::"+"::: ) (Set (Var "y"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) "}" ))); notationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); synonym "A" :::"(+)"::: "B" for "A" :::"+"::: "B"; end; theorem :: MATHMORP:1 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "B")) ($#k2_mathmorp :::"!"::: ) ")" ) ($#k2_mathmorp :::"!"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: MATHMORP:2 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "T")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ($#k1_mathmorp :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: MATHMORP:3 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_tarski :::"c="::: ) (Set (Var "B2")))) "holds" (Bool (Set (Set (Var "B1")) ($#k1_mathmorp :::"+"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B2")) ($#k1_mathmorp :::"+"::: ) (Set (Var "p"))))))) ; theorem :: MATHMORP:4 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: MATHMORP:5 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "T")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: MATHMORP:6 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "T")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: MATHMORP:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set (Var "x"))))))) ; theorem :: MATHMORP:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))))) ; theorem :: MATHMORP:9 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")))) ")" ))) ; theorem :: MATHMORP:10 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_tarski :::"c="::: ) (Set (Var "B2")))) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B1")))) & (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B2")))) ")" ))) ; theorem :: MATHMORP:11 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")))) ")" ))) ; theorem :: MATHMORP:12 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "X")))))) ; theorem :: MATHMORP:13 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Set (Var "Y")) ($#k1_mathmorp :::"+"::: ) (Set (Var "y"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set (Var "x")))) "iff" (Bool (Set (Set (Var "Y")) ($#k1_mathmorp :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" )))) ; theorem :: MATHMORP:14 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set (Var "p")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y")) ")" ) ($#k1_mathmorp :::"+"::: ) (Set (Var "p"))))))) ; theorem :: MATHMORP:15 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set (Var "p")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y")) ")" ) ($#k1_mathmorp :::"+"::: ) (Set (Var "p"))))))) ; theorem :: MATHMORP:16 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set (Var "x")) ")" ) ($#k1_mathmorp :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )))))) ; theorem :: MATHMORP:17 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set "(" (Set (Var "Y")) ($#k1_mathmorp :::"+"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y")) ")" ) ($#k1_mathmorp :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MATHMORP:18 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set "(" (Set (Var "Y")) ($#k1_mathmorp :::"+"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y")) ")" ) ($#k1_mathmorp :::"+"::: ) (Set (Var "p"))))))) ; theorem :: MATHMORP:19 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "B")) ($#k1_mathmorp :::"+"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "X"))))))) ; theorem :: MATHMORP:20 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")))))) ; theorem :: MATHMORP:21 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: MATHMORP:22 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" )))))) ; theorem :: MATHMORP:23 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set "(" (Set (Var "Y")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Z")))))) ; theorem :: MATHMORP:24 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set "(" (Set (Var "Y")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Z")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y")))))) ; theorem :: MATHMORP:25 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set "(" (Set (Var "Y")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Z")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Z")))))) ; theorem :: MATHMORP:26 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set "(" (Set (Var "Y")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Z")))))) ; theorem :: MATHMORP:27 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ) ($#k1_mathmorp :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k1_mathmorp :::"+"::: ) (Set (Var "y")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "C")) ($#k1_mathmorp :::"+"::: ) (Set (Var "y")) ")" )))))) ; theorem :: MATHMORP:28 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")) ")" ) ($#k1_mathmorp :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k1_mathmorp :::"+"::: ) (Set (Var "y")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "C")) ($#k1_mathmorp :::"+"::: ) (Set (Var "y")) ")" )))))) ; theorem :: MATHMORP:29 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "C")) ")" ))))) ; theorem :: MATHMORP:30 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "C")) ")" ))))) ; theorem :: MATHMORP:31 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")))))) ; theorem :: MATHMORP:32 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MATHMORP:33 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MATHMORP:34 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "Y")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MATHMORP:35 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "B")) ($#k6_rusub_4 :::"(+)"::: ) (Set "(" (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "B")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "X")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: MATHMORP:36 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "B")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "X")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k3_mathmorp :::"(-)"::: ) (Set "(" (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: MATHMORP:37 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set "(" (Set (Var "B")) ($#k2_mathmorp :::"!"::: ) ")" ))))) ; theorem :: MATHMORP:38 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set "(" (Set (Var "B")) ($#k2_mathmorp :::"!"::: ) ")" ))))) ; begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "X", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "X" :::"(O)"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: MATHMORP:def 4 (Set (Set "(" "X" ($#k3_mathmorp :::"(-)"::: ) "B" ")" ) ($#k6_rusub_4 :::"(+)"::: ) "B"); end; :: deftheorem defines :::"(O)"::: MATHMORP:def 4 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")))))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "X", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "X" :::"(o)"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: MATHMORP:def 5 (Set (Set "(" "X" ($#k6_rusub_4 :::"(+)"::: ) "B" ")" ) ($#k3_mathmorp :::"(-)"::: ) "B"); end; :: deftheorem defines :::"(o)"::: MATHMORP:def 5 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")))))); theorem :: MATHMORP:39 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k4_mathmorp :::"(O)"::: ) (Set "(" (Set (Var "B")) ($#k2_mathmorp :::"!"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B")))))) ; theorem :: MATHMORP:40 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k5_mathmorp :::"(o)"::: ) (Set "(" (Set (Var "B")) ($#k2_mathmorp :::"!"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B")))))) ; theorem :: MATHMORP:41 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B")))) ")" ))) ; theorem :: MATHMORP:42 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: MATHMORP:43 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")))) & (Bool (Set (Set "(" (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")))) ")" ))) ; theorem :: MATHMORP:44 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")))) ")" ))) ; theorem :: MATHMORP:45 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B")))) ")" ))) ; theorem :: MATHMORP:46 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set (Var "p")) ")" ) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "Y")) ")" ) ($#k1_mathmorp :::"+"::: ) (Set (Var "p"))))))) ; theorem :: MATHMORP:47 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set (Var "p")) ")" ) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "Y")) ")" ) ($#k1_mathmorp :::"+"::: ) (Set (Var "p"))))))) ; theorem :: MATHMORP:48 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "C")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")))))) ; theorem :: MATHMORP:49 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "C")))) "holds" (Bool (Set (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "C")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B")))))) ; theorem :: MATHMORP:50 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "Y")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y")))) & (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "Y")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y")))) ")" ))) ; theorem :: MATHMORP:51 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y")) ")" ) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "Y")))) & (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y")) ")" ) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "Y")))) ")" ))) ; theorem :: MATHMORP:52 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B")) ")" ) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B")))))) ; theorem :: MATHMORP:53 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B")) ")" ) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B")))))) ; theorem :: MATHMORP:54 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B")))))) ; theorem :: MATHMORP:55 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "B1")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B1"))))) "holds" (Bool (Set (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B1")))))) ; begin definitionlet "t" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "t" :::"(.)"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: MATHMORP:def 6 "{" (Set "(" "t" ($#k1_rlvect_1 :::"*"::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Point":::) "of" "T" : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A") "}" ; end; :: deftheorem defines :::"(.)"::: MATHMORP:def 6 : (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" )))); theorem :: MATHMORP:56 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: MATHMORP:57 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: MATHMORP:58 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Num 1) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: MATHMORP:59 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Num 2) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "X")))))) ; theorem :: MATHMORP:60 (Bool "for" (Set (Var "t")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s")) ")" ) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set "(" (Set (Var "s")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X")) ")" )))))) ; theorem :: MATHMORP:61 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "Y"))))))) ; theorem :: MATHMORP:62 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set "(" (Set (Var "X")) ($#k1_mathmorp :::"+"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X")) ")" ) ($#k1_mathmorp :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ))))))) ; theorem :: MATHMORP:63 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set "(" (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set "(" (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "Y")) ")" )))))) ; theorem :: MATHMORP:64 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X")) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set "(" (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "Y")) ")" )))))) ; theorem :: MATHMORP:65 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set "(" (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X")) ")" ) ($#k4_mathmorp :::"(O)"::: ) (Set "(" (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "Y")) ")" )))))) ; theorem :: MATHMORP:66 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set "(" (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "X")) ")" ) ($#k5_mathmorp :::"(o)"::: ) (Set "(" (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "Y")) ")" )))))) ; begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "X", "B1", "B2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "X" :::"(*)"::: "(" "B1" "," "B2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: MATHMORP:def 7 (Set (Set "(" "X" ($#k3_mathmorp :::"(-)"::: ) "B1" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" "X" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k3_mathmorp :::"(-)"::: ) "B2" ")" )); end; :: deftheorem defines :::"(*)"::: MATHMORP:def 7 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k7_mathmorp :::"(*)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B2")) ")" ))))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "X", "B1", "B2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "X" :::"(&)"::: "(" "B1" "," "B2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: MATHMORP:def 8 (Set "X" ($#k4_subset_1 :::"\/"::: ) (Set "(" "X" ($#k7_mathmorp :::"(*)"::: ) "(" "B1" "," "B2" ")" ")" )); end; :: deftheorem defines :::"(&)"::: MATHMORP:def 8 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k8_mathmorp :::"(&)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k7_mathmorp :::"(*)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ")" ))))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "X", "B1", "B2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "X" :::"(@)"::: "(" "B1" "," "B2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: MATHMORP:def 9 (Set "X" ($#k7_subset_1 :::"\"::: ) (Set "(" "X" ($#k7_mathmorp :::"(*)"::: ) "(" "B1" "," "B2" ")" ")" )); end; :: deftheorem defines :::"(@)"::: MATHMORP:def 9 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "X")) ($#k9_mathmorp :::"(@)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "X")) ($#k7_mathmorp :::"(*)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ")" ))))); theorem :: MATHMORP:67 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B1")) "," (Set (Var "X")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "X")) ($#k7_mathmorp :::"(*)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B2")))))) ; theorem :: MATHMORP:68 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B2")) "," (Set (Var "X")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "X")) ($#k7_mathmorp :::"(*)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B1")))))) ; theorem :: MATHMORP:69 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B1")) "," (Set (Var "X")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "B1")))) "holds" (Bool (Set (Set (Var "X")) ($#k7_mathmorp :::"(*)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))))) ; theorem :: MATHMORP:70 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B2")) "," (Set (Var "X")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "B2")))) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k7_mathmorp :::"(*)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: MATHMORP:71 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B1")) "," (Set (Var "X")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "B1")))) "holds" (Bool (Set (Set (Var "X")) ($#k8_mathmorp :::"(&)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: MATHMORP:72 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B2")) "," (Set (Var "X")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "B2")))) "holds" (Bool (Set (Set (Var "X")) ($#k9_mathmorp :::"(@)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: MATHMORP:73 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "B2")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "X")) ($#k9_mathmorp :::"(@)"::: ) "(" (Set (Var "B2")) "," (Set (Var "B1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k8_mathmorp :::"(&)"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; begin theorem :: MATHMORP:74 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_convex1 :::"convex"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "B"))))) ")" ))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); redefine attr "B" is :::"convex"::: means :: MATHMORP:def 10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "V" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "B") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "B")) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) "B"))); end; :: deftheorem defines :::"convex"::: MATHMORP:def 10 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_convex1 :::"convex"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "B"))))) ")" ))); theorem :: MATHMORP:75 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_convex1 :::"convex"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k2_mathmorp :::"!"::: ) ) "is" ($#v1_convex1 :::"convex"::: ) ))) ; theorem :: MATHMORP:76 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_convex1 :::"convex"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_convex1 :::"convex"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B"))) "is" ($#v1_convex1 :::"convex"::: ) ) & (Bool (Set (Set (Var "X")) ($#k3_mathmorp :::"(-)"::: ) (Set (Var "B"))) "is" ($#v1_convex1 :::"convex"::: ) ) ")" ))) ; theorem :: MATHMORP:77 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_convex1 :::"convex"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_convex1 :::"convex"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k4_mathmorp :::"(O)"::: ) (Set (Var "B"))) "is" ($#v1_convex1 :::"convex"::: ) ) & (Bool (Set (Set (Var "X")) ($#k5_mathmorp :::"(o)"::: ) (Set (Var "B"))) "is" ($#v1_convex1 :::"convex"::: ) ) ")" ))) ; theorem :: MATHMORP:78 (Bool "for" (Set (Var "t")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_convex1 :::"convex"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool (Set (Set "(" (Set (Var "s")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t")) ")" ) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "B")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set "(" (Set (Var "t")) ($#k6_mathmorp :::"(.)"::: ) (Set (Var "B")) ")" )))))) ;