:: SETFAM_1 semantic presentation begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"meet"::: "X" -> ($#m1_hidden :::"set"::: ) means :: SETFAM_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) ")" )) if (Bool "X" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"meet"::: SETFAM_1:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "X")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" ))); theorem :: SETFAM_1:1 (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: SETFAM_1:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "X"))))) ; theorem :: SETFAM_1:3 (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) ; theorem :: SETFAM_1:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: SETFAM_1:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "Z1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z1")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "Z1"))) ")" )) "holds" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "X"))))) ; theorem :: SETFAM_1:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "X"))))) ; theorem :: SETFAM_1:7 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) ; theorem :: SETFAM_1:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Z")))) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "Y"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Z")))) ; theorem :: SETFAM_1:9 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set (Var "Y")) ")" )))) ; theorem :: SETFAM_1:10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: SETFAM_1:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y"))))) ; definitionlet "SFX", "SFY" be ($#m1_hidden :::"set"::: ) ; pred "SFX" :::"is_finer_than"::: "SFY" means :: SETFAM_1:def 2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "SFX")) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) "SFY") & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))); reflexivity (Bool "for" (Set (Var "SFX")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX")))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))) ; pred "SFY" :::"is_coarser_than"::: "SFX" means :: SETFAM_1:def 3 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) "SFY")) "holds" (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "SFX") & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))); reflexivity (Bool "for" (Set (Var "SFY")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFY")))) "holds" (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFY"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))) ; end; :: deftheorem defines :::"is_finer_than"::: SETFAM_1:def 2 : (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "SFX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "SFY"))) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX")))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFY"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))) ")" )); :: deftheorem defines :::"is_coarser_than"::: SETFAM_1:def 3 : (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "SFY")) ($#r2_setfam_1 :::"is_coarser_than"::: ) (Set (Var "SFX"))) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFY")))) "holds" (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))) ")" )); theorem :: SETFAM_1:12 (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFX")) ($#r1_tarski :::"c="::: ) (Set (Var "SFY")))) "holds" (Bool (Set (Var "SFX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "SFY")))) ; theorem :: SETFAM_1:13 (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "SFY")))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "SFX"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "SFY"))))) ; theorem :: SETFAM_1:14 (Bool "for" (Set (Var "SFY")) "," (Set (Var "SFX")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFY")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "SFY")) ($#r2_setfam_1 :::"is_coarser_than"::: ) (Set (Var "SFX")))) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "SFX"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "SFY"))))) ; theorem :: SETFAM_1:15 (Bool "for" (Set (Var "SFX")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "SFX")))) ; theorem :: SETFAM_1:16 (Bool "for" (Set (Var "SFX")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "SFX")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: SETFAM_1:17 (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "," (Set (Var "SFZ")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "SFY"))) & (Bool (Set (Var "SFY")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "SFZ")))) "holds" (Bool (Set (Var "SFX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "SFZ")))) ; theorem :: SETFAM_1:18 (Bool "for" (Set (Var "Y")) "," (Set (Var "SFX")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "Y")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX")))) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))))) ; theorem :: SETFAM_1:19 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "SFX")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX"))) "or" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) "or" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))) ; definitionlet "SFX", "SFY" be ($#m1_hidden :::"set"::: ) ; func :::"UNION"::: "(" "SFX" "," "SFY" ")" -> ($#m1_hidden :::"set"::: ) means :: SETFAM_1:def 4 (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "SFX") & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) "SFY") & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")))) ")" )) ")" )); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFY"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")))) ")" )) ")" ) ")" )) "holds" (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFY"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")))) ")" )) ")" )))) ; func :::"INTERSECTION"::: "(" "SFX" "," "SFY" ")" -> ($#m1_hidden :::"set"::: ) means :: SETFAM_1:def 5 (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "SFX") & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) "SFY") & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")))) ")" )) ")" )); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFY"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")))) ")" )) ")" ) ")" )) "holds" (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFY"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")))) ")" )) ")" )))) ; func :::"DIFFERENCE"::: "(" "SFX" "," "SFY" ")" -> ($#m1_hidden :::"set"::: ) means :: SETFAM_1:def 6 (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "SFX") & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) "SFY") & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")))) ")" )) ")" )); end; :: deftheorem defines :::"UNION"::: SETFAM_1:def 4 : (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_setfam_1 :::"UNION"::: ) "(" (Set (Var "SFX")) "," (Set (Var "SFY")) ")" )) "iff" (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFY"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")))) ")" )) ")" )) ")" ))); :: deftheorem defines :::"INTERSECTION"::: SETFAM_1:def 5 : (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "SFX")) "," (Set (Var "SFY")) ")" )) "iff" (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFY"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")))) ")" )) ")" )) ")" ))); :: deftheorem defines :::"DIFFERENCE"::: SETFAM_1:def 6 : (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_setfam_1 :::"DIFFERENCE"::: ) "(" (Set (Var "SFX")) "," (Set (Var "SFY")) ")" )) "iff" (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "SFX"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "SFY"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")))) ")" )) ")" )) ")" ))); theorem :: SETFAM_1:20 (Bool "for" (Set (Var "SFX")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "SFX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set ($#k2_setfam_1 :::"UNION"::: ) "(" (Set (Var "SFX")) "," (Set (Var "SFX")) ")" ))) ; theorem :: SETFAM_1:21 (Bool "for" (Set (Var "SFX")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "SFX")) "," (Set (Var "SFX")) ")" ) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "SFX")))) ; theorem :: SETFAM_1:22 (Bool "for" (Set (Var "SFX")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_setfam_1 :::"DIFFERENCE"::: ) "(" (Set (Var "SFX")) "," (Set (Var "SFX")) ")" ) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "SFX")))) ; theorem :: SETFAM_1:23 (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFX")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "SFY")))) "holds" (Bool (Set (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set (Var "SFX")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set (Var "SFY")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "SFX")) "," (Set (Var "SFY")) ")" ")" )))) ; theorem :: SETFAM_1:24 (Bool "for" (Set (Var "X")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFY")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set (Var "SFY")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k2_setfam_1 :::"UNION"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "SFY")) ")" ")" )))) ; theorem :: SETFAM_1:25 (Bool "for" (Set (Var "X")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "SFY")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "SFY")) ")" ")" )))) ; theorem :: SETFAM_1:26 (Bool "for" (Set (Var "X")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFY")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "SFY")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k4_setfam_1 :::"DIFFERENCE"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "SFY")) ")" ")" )))) ; theorem :: SETFAM_1:27 (Bool "for" (Set (Var "X")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFY")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set (Var "SFY")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k4_setfam_1 :::"DIFFERENCE"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "SFY")) ")" ")" )))) ; theorem :: SETFAM_1:28 (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "SFX")) "," (Set (Var "SFY")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "SFX")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "SFY")) ")" )))) ; theorem :: SETFAM_1:29 (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "SFX")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "SFY")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set (Var "SFX")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set (Var "SFY")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k2_setfam_1 :::"UNION"::: ) "(" (Set (Var "SFX")) "," (Set (Var "SFY")) ")" ")" )))) ; theorem :: SETFAM_1:30 (Bool "for" (Set (Var "SFX")) "," (Set (Var "SFY")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k4_setfam_1 :::"DIFFERENCE"::: ) "(" (Set (Var "SFX")) "," (Set (Var "SFY")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set (Var "SFX")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set (Var "SFY")) ")" )))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; mode Subset-Family of "D" is ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "D" ")" ); end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "D")); :: original: :::"union"::: redefine func :::"union"::: "F" -> ($#m1_subset_1 :::"Subset":::) "of" "D"; end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "D")); :: original: :::"meet"::: redefine func :::"meet"::: "F" -> ($#m1_subset_1 :::"Subset":::) "of" "D"; end; theorem :: SETFAM_1:31 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "D")) "st" (Bool (Bool "(" "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) ")" )) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "D")); func :::"COMPLEMENT"::: "F" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "D" means :: SETFAM_1:def 7 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" "D" "holds" (Bool "(" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) "F") ")" )); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "D")) "st" (Bool (Bool "(" "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ))) ; end; :: deftheorem defines :::"COMPLEMENT"::: SETFAM_1:def 7 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) ")" ))); theorem :: SETFAM_1:32 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: SETFAM_1:33 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "D")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F")) ")" ))))) ; theorem :: SETFAM_1:34 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "D")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F")) ")" ))))) ; begin theorem :: SETFAM_1:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )))) ; theorem :: SETFAM_1:36 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))))) ; theorem :: SETFAM_1:37 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) "iff" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "G")))) ")" ))) ; theorem :: SETFAM_1:38 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))))) ; theorem :: SETFAM_1:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set "(" (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "G")) ")" ))))) ; theorem :: SETFAM_1:40 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); cluster (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"with_non-empty_elements"::: means :: SETFAM_1:def 8 (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) "IT")); end; :: deftheorem defines :::"with_non-empty_elements"::: SETFAM_1:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ) "iff" (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; let "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) "A" "," "B" ($#k2_tarski :::"}"::: ) ) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; let "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_enumset1 :::"{"::: ) "A" "," "B" "," "C" ($#k1_enumset1 :::"}"::: ) ) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_enumset1 :::"{"::: ) "A" "," "B" "," "C" "," "D" ($#k2_enumset1 :::"}"::: ) ) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; let "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_enumset1 :::"{"::: ) "A" "," "B" "," "C" "," "D" "," "E" ($#k3_enumset1 :::"}"::: ) ) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_enumset1 :::"{"::: ) "A" "," "B" "," "C" "," "D" "," "E" "," "F" ($#k4_enumset1 :::"}"::: ) ) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; let "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_enumset1 :::"{"::: ) "A" "," "B" "," "C" "," "D" "," "E" "," "F" "," "G" ($#k5_enumset1 :::"}"::: ) ) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; let "H" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k6_enumset1 :::"{"::: ) "A" "," "B" "," "C" "," "D" "," "E" "," "F" "," "G" "," "H" ($#k6_enumset1 :::"}"::: ) ) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; let "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_enumset1 :::"{"::: ) "A" "," "B" "," "C" "," "D" "," "E" "," "F" "," "G" "," "H" "," "I" ($#k7_enumset1 :::"}"::: ) ) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; let "J" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_enumset1 :::"{"::: ) "A" "," "B" "," "C" "," "D" "," "E" "," "F" "," "G" "," "H" "," "I" "," "J" ($#k8_enumset1 :::"}"::: ) ) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; end; registrationlet "A", "B" be ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k2_xboole_0 :::"\/"::: ) "B") -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; end; theorem :: SETFAM_1:41 (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) ; theorem :: SETFAM_1:42 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")) ")" ))) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "Y")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))))) ; definitionlet "M" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "M")); func :::"Intersect"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "M" equals :: SETFAM_1:def 9 (Set ($#k6_setfam_1 :::"meet"::: ) "B") if (Bool "B" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise "M"; end; :: deftheorem defines :::"Intersect"::: SETFAM_1:def 9 : (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "M")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "B")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "M"))) ")" ")" ))); theorem :: SETFAM_1:43 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) ")" ))) ; theorem :: SETFAM_1:44 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "J"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "H")))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; attr "E" is :::"empty-membered"::: means :: SETFAM_1:def 10 (Bool "for" (Set (Var "x")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) "E"))); end; :: deftheorem defines :::"empty-membered"::: SETFAM_1:def 10 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "E")) "is" ($#v2_setfam_1 :::"empty-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))))) ")" )); notationlet "E" be ($#m1_hidden :::"set"::: ) ; antonym :::"with_non-empty_element"::: "E" for :::"empty-membered"::: ; end; registration cluster ($#v2_setfam_1 :::"with_non-empty_element"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v2_setfam_1 :::"with_non-empty_element"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_tarski :::"union"::: ) "D") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) -> ($#v2_setfam_1 :::"with_non-empty_element"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode :::"Cover"::: "of" "X" -> ($#m1_hidden :::"set"::: ) means :: SETFAM_1:def 11 (Bool "X" ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) it)); end; :: deftheorem defines :::"Cover"::: SETFAM_1:def 11 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "b2")))) ")" ))); theorem :: SETFAM_1:45 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ))) ; theorem :: SETFAM_1:46 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "F" is :::"with_proper_subsets"::: means :: SETFAM_1:def 12 (Bool (Bool "not" "X" ($#r2_hidden :::"in"::: ) "F")); end; :: deftheorem defines :::"with_proper_subsets"::: SETFAM_1:def 12 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_setfam_1 :::"with_proper_subsets"::: ) ) "iff" (Bool (Bool "not" (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" ))); theorem :: SETFAM_1:47 (Bool "for" (Set (Var "TS")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_setfam_1 :::"with_proper_subsets"::: ) ) & (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "G")) "is" ($#v3_setfam_1 :::"with_proper_subsets"::: ) ))) ; registrationlet "TS" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v3_setfam_1 :::"with_proper_subsets"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "TS" ")" )); end; theorem :: SETFAM_1:48 (Bool "for" (Set (Var "TS")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v3_setfam_1 :::"with_proper_subsets"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TS")) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#v3_setfam_1 :::"with_proper_subsets"::: ) ))) ; registration cluster ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) -> ($#v2_setfam_1 :::"with_non-empty_element"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"bool"::: redefine func :::"bool"::: "X" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; end; theorem :: SETFAM_1:49 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))))) ;