:: MIDSP_1 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"MidStr"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"MidStr":::(# :::"carrier":::, :::"MIDPOINT"::: #) -> ($#l1_midsp_1 :::"MidStr"::: ) ; sel :::"MIDPOINT"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_midsp_1 :::"MidStr"::: ) ; end; definitionlet "MS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "MS")); func "a" :::"@"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "MS" equals :: MIDSP_1:def 1 (Set (Set "the" ($#u1_midsp_1 :::"MIDPOINT"::: ) "of" "MS") ($#k5_binop_1 :::"."::: ) "(" "a" "," "b" ")" ); end; :: deftheorem defines :::"@"::: MIDSP_1:def 1 : (Bool "for" (Set (Var "MS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MS")) "holds" (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_midsp_1 :::"MIDPOINT"::: ) "of" (Set (Var "MS"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))); definitionfunc :::"Example"::: -> ($#l1_midsp_1 :::"MidStr"::: ) equals :: MIDSP_1:def 2 (Set ($#g1_midsp_1 :::"MidStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "#)" ); end; :: deftheorem defines :::"Example"::: MIDSP_1:def 2 : (Bool (Set ($#k2_midsp_1 :::"Example"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_midsp_1 :::"MidStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "#)" )); registration cluster (Set ($#k2_midsp_1 :::"Example"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_midsp_1 :::"strict"::: ) ; end; theorem :: MIDSP_1:1 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k2_midsp_1 :::"Example"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: MIDSP_1:2 (Bool (Set "the" ($#u1_midsp_1 :::"MIDPOINT"::: ) "of" (Set ($#k2_midsp_1 :::"Example"::: ) )) ($#r1_funct_2 :::"="::: ) (Set ($#k9_funct_5 :::"op2"::: ) )) ; theorem :: MIDSP_1:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_midsp_1 :::"Example"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_funct_5 :::"op2"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; theorem :: MIDSP_1:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_midsp_1 :::"Example"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "a")))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b")) ")" ) ($#k1_midsp_1 :::"@"::: ) (Set "(" (Set (Var "c")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "c")) ")" ) ($#k1_midsp_1 :::"@"::: ) (Set "(" (Set (Var "b")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "d")) ")" ))) & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_midsp_1 :::"Example"::: ) ) "st" (Bool (Set (Set (Var "x")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" )) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) ; attr "IT" is :::"MidSp-like"::: means :: MIDSP_1:def 3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "a")))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b")) ")" ) ($#k1_midsp_1 :::"@"::: ) (Set "(" (Set (Var "c")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "c")) ")" ) ($#k1_midsp_1 :::"@"::: ) (Set "(" (Set (Var "b")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "d")) ")" ))) & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Set (Var "x")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" )); end; :: deftheorem defines :::"MidSp-like"::: MIDSP_1:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_midsp_1 :::"MidSp-like"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "a")))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b")) ")" ) ($#k1_midsp_1 :::"@"::: ) (Set "(" (Set (Var "c")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "c")) ")" ) ($#k1_midsp_1 :::"@"::: ) (Set "(" (Set (Var "b")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "d")) ")" ))) & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Set (Var "x")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_midsp_1 :::"strict"::: ) ($#v2_midsp_1 :::"MidSp-like"::: ) for ($#l1_midsp_1 :::"MidStr"::: ) ; end; definitionmode MidSp is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_1 :::"MidStr"::: ) ; end; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); :: original: :::"@"::: redefine func "a" :::"@"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "M"; commutativity (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")) "holds" (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "a"))))) ; end; theorem :: MIDSP_1:5 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b")) ")" ) ($#k3_midsp_1 :::"@"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "c")) ")" ) ($#k3_midsp_1 :::"@"::: ) (Set "(" (Set (Var "b")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "c")) ")" ))))) ; theorem :: MIDSP_1:6 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set "(" (Set (Var "b")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b")) ")" ) ($#k3_midsp_1 :::"@"::: ) (Set "(" (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "c")) ")" ))))) ; theorem :: MIDSP_1:7 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: MIDSP_1:8 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "x9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))))) ; theorem :: MIDSP_1:9 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "x9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "x9"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))))) ; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); pred "a" "," "b" :::"@@"::: "c" "," "d" means :: MIDSP_1:def 4 (Bool (Set "a" ($#k3_midsp_1 :::"@"::: ) "d") ($#r1_hidden :::"="::: ) (Set "b" ($#k3_midsp_1 :::"@"::: ) "c")); end; :: deftheorem defines :::"@@"::: MIDSP_1:def 4 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "c")))) ")" ))); theorem :: MIDSP_1:10 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "b")) "," (Set (Var "b"))))) ; theorem :: MIDSP_1:11 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: MIDSP_1:12 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "b")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: MIDSP_1:13 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "c")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: MIDSP_1:14 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: MIDSP_1:15 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "c")) "," (Set (Var "d")))))) ; theorem :: MIDSP_1:16 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "c")) "," (Set (Var "d9")))) "holds" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "d9"))))) ; theorem :: MIDSP_1:17 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: MIDSP_1:18 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "b9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "a9")) "," (Set (Var "c9"))))) ; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) ($#k2_zfmisc_1 :::":]"::: ) ); pred "p" :::"##"::: "q" means :: MIDSP_1:def 5 (Bool (Set "p" ($#k2_domain_1 :::"`1"::: ) ) "," (Set "p" ($#k3_domain_1 :::"`2"::: ) ) ($#r1_midsp_1 :::"@@"::: ) (Set "q" ($#k2_domain_1 :::"`1"::: ) ) "," (Set "q" ($#k3_domain_1 :::"`2"::: ) )); reflexivity (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_midsp_1 :::"@@"::: ) (Set (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) ))) ; symmetry (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_midsp_1 :::"@@"::: ) (Set (Set (Var "q")) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set (Var "q")) ($#k3_domain_1 :::"`2"::: ) ))) "holds" (Bool (Set (Set (Var "q")) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set (Var "q")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_midsp_1 :::"@@"::: ) (Set (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) ))) ; end; :: deftheorem defines :::"##"::: MIDSP_1:def 5 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "q"))) "iff" (Bool (Set (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_midsp_1 :::"@@"::: ) (Set (Set (Var "q")) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set (Var "q")) ($#k3_domain_1 :::"`2"::: ) )) ")" ))); theorem :: MIDSP_1:19 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_midsp_1 :::"##"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) )))) ; theorem :: MIDSP_1:20 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_midsp_1 :::"##"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_midsp_1 :::"@@"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: MIDSP_1:21 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "q")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "r"))))) ; theorem :: MIDSP_1:22 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "r"))) & (Bool (Set (Var "q")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "q"))))) ; theorem :: MIDSP_1:23 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "r"))))) ; theorem :: MIDSP_1:24 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "q")))) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "r")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "q"))) ")" ))) ; theorem :: MIDSP_1:25 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Var "q")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "p"))) "}" "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) )))) ; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) ($#k2_zfmisc_1 :::":]"::: ) ); func "p" :::"~"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) ) equals :: MIDSP_1:def 6 "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Var "q")) ($#r2_midsp_1 :::"##"::: ) "p") "}" ; end; :: deftheorem defines :::"~"::: MIDSP_1:def 6 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k4_midsp_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Var "q")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "p"))) "}" ))); registrationlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) ($#k2_zfmisc_1 :::":]"::: ) ); cluster (Set "p" ($#k4_midsp_1 :::"~"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: MIDSP_1:26 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "p")) ($#k4_midsp_1 :::"~"::: ) )) "iff" (Bool (Set (Var "r")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "p"))) ")" ))) ; theorem :: MIDSP_1:27 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "p")) ($#k4_midsp_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k4_midsp_1 :::"~"::: ) )))) ; theorem :: MIDSP_1:28 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k4_midsp_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k4_midsp_1 :::"~"::: ) ))) "holds" (Bool (Set (Var "p")) ($#r2_midsp_1 :::"##"::: ) (Set (Var "q"))))) ; theorem :: MIDSP_1:29 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) ($#k4_midsp_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ($#k4_midsp_1 :::"~"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "c")))))) ; theorem :: MIDSP_1:30 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "p")) ($#k4_midsp_1 :::"~"::: ) )))) ; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); mode :::"Vector"::: "of" "M" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) ) means :: MIDSP_1:def 7 (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_midsp_1 :::"~"::: ) ))); end; :: deftheorem defines :::"Vector"::: MIDSP_1:def 7 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M"))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_midsp_1 :::"~"::: ) ))) ")" ))); definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"~"::: redefine func "p" :::"~"::: -> ($#m1_midsp_1 :::"Vector"::: ) "of" "M"; end; theorem :: MIDSP_1:31 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "ex" (Set (Var "u")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) "st" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "u"))) "iff" (Bool (Set (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) )) ")" )))) ; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); func :::"ID"::: "M" -> ($#m1_midsp_1 :::"Vector"::: ) "of" "M" equals :: MIDSP_1:def 8 "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) )) "}" ; end; :: deftheorem defines :::"ID"::: MIDSP_1:def 8 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) "holds" (Bool (Set ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) )) "}" )); theorem :: MIDSP_1:32 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) ($#k5_midsp_1 :::"~"::: ) )))) ; theorem :: MIDSP_1:33 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "w9")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) "st" (Bool (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_midsp_1 :::"~"::: ) )) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k5_midsp_1 :::"~"::: ) )) & (Bool (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "q")) ($#k3_domain_1 :::"`2"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#k5_midsp_1 :::"~"::: ) )) ")" )) & (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_midsp_1 :::"~"::: ) )) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k5_midsp_1 :::"~"::: ) )) & (Bool (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Var "w9")) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "q")) ($#k3_domain_1 :::"`2"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#k5_midsp_1 :::"~"::: ) )) ")" ))) "holds" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "w9"))))) ; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "u", "v" be ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Const "M")); func "u" :::"+"::: "v" -> ($#m1_midsp_1 :::"Vector"::: ) "of" "M" means :: MIDSP_1:def 9 (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool "u" ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_midsp_1 :::"~"::: ) )) & (Bool "v" ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k5_midsp_1 :::"~"::: ) )) & (Bool (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k2_domain_1 :::"`1"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "q")) ($#k3_domain_1 :::"`2"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#k5_midsp_1 :::"~"::: ) )) ")" )); end; :: deftheorem defines :::"+"::: MIDSP_1:def 9 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "b4")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "v")))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_midsp_1 :::"~"::: ) )) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k5_midsp_1 :::"~"::: ) )) & (Bool (Set (Set (Var "p")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "p")) ($#k2_domain_1 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "q")) ($#k3_domain_1 :::"`2"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#k5_midsp_1 :::"~"::: ) )) ")" )) ")" ))); theorem :: MIDSP_1:34 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "u")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) ($#k5_midsp_1 :::"~"::: ) )))))) ; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); func :::"vect"::: "(" "a" "," "b" ")" -> ($#m1_midsp_1 :::"Vector"::: ) "of" "M" equals :: MIDSP_1:def 10 (Set (Set ($#k1_domain_1 :::"["::: ) "a" "," "b" ($#k1_domain_1 :::"]"::: ) ) ($#k5_midsp_1 :::"~"::: ) ); end; :: deftheorem defines :::"vect"::: MIDSP_1:def 10 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) ($#k5_midsp_1 :::"~"::: ) )))); theorem :: MIDSP_1:35 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "u")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))))) ; theorem :: MIDSP_1:36 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_midsp_1 :::"##"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" )))) ; theorem :: MIDSP_1:37 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ))) "holds" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "c")))))) ; theorem :: MIDSP_1:38 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "b")) "," (Set (Var "b")) ")" )))) ; theorem :: MIDSP_1:39 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: MIDSP_1:40 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k7_midsp_1 :::"+"::: ) (Set "(" ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )))) ; theorem :: MIDSP_1:41 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set "(" (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_midsp_1 :::"##"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b")) ")" ) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) )))) ; theorem :: MIDSP_1:42 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b")) ")" ) ")" ")" ) ($#k7_midsp_1 :::"+"::: ) (Set "(" ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; theorem :: MIDSP_1:43 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" (Set (Var "u")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "v")) ")" ) ($#k7_midsp_1 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k7_midsp_1 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "w")) ")" ))))) ; theorem :: MIDSP_1:44 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "u")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "u")) ($#k7_midsp_1 :::"+"::: ) (Set "(" ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "u"))))) ; theorem :: MIDSP_1:45 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "u")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) (Bool "ex" (Set (Var "v")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) "st" (Bool (Set (Set (Var "u")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M"))))))) ; theorem :: MIDSP_1:46 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "u")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "u")))))) ; theorem :: MIDSP_1:47 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "u")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "w"))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w"))))) ; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "u" be ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Const "M")); func :::"-"::: "u" -> ($#m1_midsp_1 :::"Vector"::: ) "of" "M" means :: MIDSP_1:def 11 (Bool (Set "u" ($#k7_midsp_1 :::"+"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k6_midsp_1 :::"ID"::: ) "M")); end; :: deftheorem defines :::"-"::: MIDSP_1:def 11 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "u")) "," (Set (Var "b3")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_midsp_1 :::"-"::: ) (Set (Var "u")))) "iff" (Bool (Set (Set (Var "u")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M")))) ")" ))); definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); func :::"setvect"::: "M" -> ($#m1_hidden :::"set"::: ) equals :: MIDSP_1:def 12 "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Var "X")) "is" ($#m1_midsp_1 :::"Vector"::: ) "of" "M") "}" ; end; :: deftheorem defines :::"setvect"::: MIDSP_1:def 12 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) "holds" (Bool (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool (Set (Var "X")) "is" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M"))) "}" )); theorem :: MIDSP_1:48 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M")))) ")" ))) ; registrationlet "M" be ($#l1_midsp_1 :::"MidSp":::); cluster (Set ($#k10_midsp_1 :::"setvect"::: ) "M") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "u1", "v1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Const "M"))); func "u1" :::"+"::: "v1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) "M") means :: MIDSP_1:def 13 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" "M" "st" (Bool (Bool "u1" ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool "v1" ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "v"))))); end; :: deftheorem defines :::"+"::: MIDSP_1:def 13 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u1")) ($#k11_midsp_1 :::"+"::: ) (Set (Var "v1")))) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "v"))))) ")" ))); theorem :: MIDSP_1:49 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "u1")) ($#k11_midsp_1 :::"+"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k11_midsp_1 :::"+"::: ) (Set (Var "u1")))))) ; theorem :: MIDSP_1:50 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set "(" (Set (Var "u1")) ($#k11_midsp_1 :::"+"::: ) (Set (Var "v1")) ")" ) ($#k11_midsp_1 :::"+"::: ) (Set (Var "w1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u1")) ($#k11_midsp_1 :::"+"::: ) (Set "(" (Set (Var "v1")) ($#k11_midsp_1 :::"+"::: ) (Set (Var "w1")) ")" ))))) ; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); func :::"addvect"::: "M" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k10_midsp_1 :::"setvect"::: ) "M" ")" ) means :: MIDSP_1:def 14 (Bool "for" (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) "M") "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u1")) "," (Set (Var "v1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "u1")) ($#k11_midsp_1 :::"+"::: ) (Set (Var "v1"))))); end; :: deftheorem defines :::"addvect"::: MIDSP_1:def 14 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_midsp_1 :::"addvect"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "u1")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "u1")) "," (Set (Var "v1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "u1")) ($#k11_midsp_1 :::"+"::: ) (Set (Var "v1"))))) ")" ))); theorem :: MIDSP_1:51 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M"))) (Bool "ex" (Set (Var "T")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M"))) "st" (Bool (Set (Set (Var "W")) ($#k11_midsp_1 :::"+"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M"))))))) ; theorem :: MIDSP_1:52 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "W")) "," (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M"))) "st" (Bool (Bool (Set (Set (Var "W")) ($#k11_midsp_1 :::"+"::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "W")) ($#k11_midsp_1 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2"))))) ; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); func :::"complvect"::: "M" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k10_midsp_1 :::"setvect"::: ) "M" ")" ) means :: MIDSP_1:def 15 (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) "M") "holds" (Bool (Set (Set (Var "W")) ($#k11_midsp_1 :::"+"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "W")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_midsp_1 :::"ID"::: ) "M"))); end; :: deftheorem defines :::"complvect"::: MIDSP_1:def 15 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_midsp_1 :::"complvect"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "W")) ($#k11_midsp_1 :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "W")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M"))))) ")" ))); definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); func :::"zerovect"::: "M" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_midsp_1 :::"setvect"::: ) "M") equals :: MIDSP_1:def 16 (Set ($#k6_midsp_1 :::"ID"::: ) "M"); end; :: deftheorem defines :::"zerovect"::: MIDSP_1:def 16 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) "holds" (Bool (Set ($#k14_midsp_1 :::"zerovect"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M"))))); definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); func :::"vectgroup"::: "M" -> ($#l2_algstr_0 :::"addLoopStr"::: ) equals :: MIDSP_1:def 17 (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "(" ($#k10_midsp_1 :::"setvect"::: ) "M" ")" ) "," (Set "(" ($#k12_midsp_1 :::"addvect"::: ) "M" ")" ) "," (Set "(" ($#k14_midsp_1 :::"zerovect"::: ) "M" ")" ) "#)" ); end; :: deftheorem defines :::"vectgroup"::: MIDSP_1:def 17 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) "holds" (Bool (Set ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "(" ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k12_midsp_1 :::"addvect"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k14_midsp_1 :::"zerovect"::: ) (Set (Var "M")) ")" ) "#)" ))); registrationlet "M" be ($#l1_midsp_1 :::"MidSp":::); cluster (Set ($#k15_midsp_1 :::"vectgroup"::: ) "M") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ; end; theorem :: MIDSP_1:53 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_midsp_1 :::"setvect"::: ) (Set (Var "M"))))) ; theorem :: MIDSP_1:54 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) "holds" (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k12_midsp_1 :::"addvect"::: ) (Set (Var "M"))))) ; theorem :: MIDSP_1:55 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k14_midsp_1 :::"zerovect"::: ) (Set (Var "M"))))) ; theorem :: MIDSP_1:56 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) "holds" (Bool "(" (Bool (Set ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M"))) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M"))) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M"))) "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) & (Bool (Set ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M"))) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) ")" )) ;