:: INTERVA1 semantic presentation begin definitionlet "U" be ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "U")); func :::"Inter"::: "(" "X" "," "Y" ")" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "U" equals :: INTERVA1:def 1 "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" "U" : (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) "Y") ")" ) "}" ; end; :: deftheorem defines :::"Inter"::: INTERVA1:def 1 : (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "holds" (Bool (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) : (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) "}" ))); theorem :: INTERVA1:1 (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) ")" )))) ; theorem :: INTERVA1:2 (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) ")" ))) ; theorem :: INTERVA1:3 (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Bool "not" (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: INTERVA1:4 (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))))) ; theorem :: INTERVA1:5 (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))) ; theorem :: INTERVA1:6 (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "C")) "," (Set (Var "D")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "D"))) ")" ))) ; theorem :: INTERVA1:7 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "holds" (Bool (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "U")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: INTERVA1:8 (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "holds" (Bool (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) )))) ; definitionlet "U" be ($#m1_hidden :::"set"::: ) ; mode :::"IntervalSet"::: "of" "U" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "U" means :: INTERVA1:def 2 (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "U" "st" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))); end; :: deftheorem defines :::"IntervalSet"::: INTERVA1:def 2 : (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "U")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U"))) "iff" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) ")" ))); theorem :: INTERVA1:9 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")))) ; theorem :: INTERVA1:10 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U"))))) ; definitionlet "U" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "U")); :: original: :::"Inter"::: redefine func :::"Inter"::: "(" "A" "," "B" ")" -> ($#m1_interva1 :::"IntervalSet"::: ) "of" "U"; end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_interva1 :::"IntervalSet"::: ) "of" "U"; end; theorem :: INTERVA1:11 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U"))) "iff" (Bool "ex" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool "(" (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" )) ")" )) ")" ))) ; theorem :: INTERVA1:12 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Var "B1")) ($#r1_tarski :::"c="::: ) (Set (Var "B2")))) "holds" (Bool (Set ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set "(" ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ")" ) "," (Set "(" ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "C")) where C "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) : (Bool "(" (Bool (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B1"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A2")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B2")))) ")" ) "}" ))) ; theorem :: INTERVA1:13 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Var "B1")) ($#r1_tarski :::"c="::: ) (Set (Var "B2")))) "holds" (Bool (Set ($#k2_setfam_1 :::"UNION"::: ) "(" (Set "(" ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ")" ) "," (Set "(" ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "C")) where C "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) : (Bool "(" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B1"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A2")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2")))) ")" ) "}" ))) ; definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Const "U")); func "A" :::"_/\_"::: "B" -> ($#m1_interva1 :::"IntervalSet"::: ) "of" "U" equals :: INTERVA1:def 3 (Set ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" "A" "," "B" ")" ); func "A" :::"_\/_"::: "B" -> ($#m1_interva1 :::"IntervalSet"::: ) "of" "U" equals :: INTERVA1:def 4 (Set ($#k2_setfam_1 :::"UNION"::: ) "(" "A" "," "B" ")" ); end; :: deftheorem defines :::"_/\_"::: INTERVA1:def 3 : (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )))); :: deftheorem defines :::"_\/_"::: INTERVA1:def 4 : (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_setfam_1 :::"UNION"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )))); registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Const "U")); cluster (Set "A" ($#k3_interva1 :::"_/\_"::: ) "B") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set "A" ($#k4_interva1 :::"_\/_"::: ) "B") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Const "U")); func "A" :::"``1"::: -> ($#m1_subset_1 :::"Subset":::) "of" "U" means :: INTERVA1:def 5 (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "U" "st" (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" it "," (Set (Var "B")) ")" ))); func "A" :::"``2"::: -> ($#m1_subset_1 :::"Subset":::) "of" "U" means :: INTERVA1:def 6 (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "U" "st" (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "B")) "," it ")" ))); end; :: deftheorem defines :::"``1"::: INTERVA1:def 5 : (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_interva1 :::"``1"::: ) )) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "b3")) "," (Set (Var "B")) ")" ))) ")" )))); :: deftheorem defines :::"``2"::: INTERVA1:def 6 : (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_interva1 :::"``2"::: ) )) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "B")) "," (Set (Var "b3")) ")" ))) ")" )))); theorem :: INTERVA1:14 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Set (Var "A")) ($#k5_interva1 :::"``1"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k6_interva1 :::"``2"::: ) )) ")" ) ")" )))) ; theorem :: INTERVA1:15 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" (Set (Var "A")) ($#k5_interva1 :::"``1"::: ) ")" ) "," (Set "(" (Set (Var "A")) ($#k6_interva1 :::"``2"::: ) ")" ) ")" )))) ; theorem :: INTERVA1:16 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k5_interva1 :::"``1"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k6_interva1 :::"``2"::: ) )))) ; theorem :: INTERVA1:17 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" (Set "(" (Set (Var "A")) ($#k5_interva1 :::"``1"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k5_interva1 :::"``1"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "A")) ($#k6_interva1 :::"``2"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k6_interva1 :::"``2"::: ) ")" ) ")" ) ")" )))) ; theorem :: INTERVA1:18 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" (Set "(" (Set (Var "A")) ($#k5_interva1 :::"``1"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k5_interva1 :::"``1"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "A")) ($#k6_interva1 :::"``2"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k6_interva1 :::"``2"::: ) ")" ) ")" ) ")" )))) ; definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Const "U")); :: original: :::"="::: redefine pred "A" :::"="::: "B" means :: INTERVA1:def 7 (Bool "(" (Bool (Set "A" ($#k5_interva1 :::"``1"::: ) ) ($#r1_hidden :::"="::: ) (Set "B" ($#k5_interva1 :::"``1"::: ) )) & (Bool (Set "A" ($#k6_interva1 :::"``2"::: ) ) ($#r1_hidden :::"="::: ) (Set "B" ($#k6_interva1 :::"``2"::: ) )) ")" ); end; :: deftheorem defines :::"="::: INTERVA1:def 7 : (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_interva1 :::"="::: ) (Set (Var "B"))) "iff" (Bool "(" (Bool (Set (Set (Var "A")) ($#k5_interva1 :::"``1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k5_interva1 :::"``1"::: ) )) & (Bool (Set (Set (Var "A")) ($#k6_interva1 :::"``2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k6_interva1 :::"``2"::: ) )) ")" ) ")" ))); theorem :: INTERVA1:19 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "A"))) ($#r1_interva1 :::"="::: ) (Set (Var "A"))))) ; theorem :: INTERVA1:20 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "A"))) ($#r1_interva1 :::"="::: ) (Set (Var "A"))))) ; theorem :: INTERVA1:21 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "B"))) ($#r1_interva1 :::"="::: ) (Set (Set (Var "B")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "A")))))) ; theorem :: INTERVA1:22 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "B"))) ($#r1_interva1 :::"="::: ) (Set (Set (Var "B")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "A")))))) ; theorem :: INTERVA1:23 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "B")) ")" ) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "C"))) ($#r1_interva1 :::"="::: ) (Set (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set "(" (Set (Var "B")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "C")) ")" ))))) ; theorem :: INTERVA1:24 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "B")) ")" ) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "C"))) ($#r1_interva1 :::"="::: ) (Set (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set "(" (Set (Var "B")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "C")) ")" ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "F" is :::"ordered"::: means :: INTERVA1:def 8 (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "F") & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) "F") "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" ) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"ordered"::: INTERVA1:def 8 : (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" ($#v1_interva1 :::"ordered"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" ) ")" ) ")" ) ")" )) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_interva1 :::"ordered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK1_ZFMISC_1("X")))); end; theorem :: INTERVA1:25 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_interva1 :::"ordered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "U"))))) ; theorem :: INTERVA1:26 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Var "A")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_interva1 :::"ordered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "U"))))) ; notationlet "X" be ($#m1_hidden :::"set"::: ) ; synonym :::"min"::: "X" for :::"meet"::: "X"; synonym :::"max"::: "X" for :::"union"::: "X"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_interva1 :::"ordered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); :: original: :::"min"::: redefine func :::"min"::: "F" -> ($#m2_subset_1 :::"Element"::: ) "of" "F"; :: original: :::"max"::: redefine func :::"max"::: "F" -> ($#m2_subset_1 :::"Element"::: ) "of" "F"; end; theorem :: INTERVA1:27 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_interva1 :::"ordered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k7_interva1 :::"min"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k8_interva1 :::"max"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" )))) ; theorem :: INTERVA1:28 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_interva1 :::"ordered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set ($#k7_interva1 :::"min"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k8_interva1 :::"max"::: ) (Set (Var "A")))) ")" ) ")" ))) ; theorem :: INTERVA1:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_interva1 :::"ordered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_setfam_1 :::"UNION"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set "(" ($#k2_setfam_1 :::"UNION"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "," (Set "(" ($#k2_setfam_1 :::"UNION"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" ) ")" )))) ; theorem :: INTERVA1:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_interva1 :::"ordered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_setfam_1 :::"UNION"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_setfam_1 :::"UNION"::: ) "(" (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "," (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" ) ")" )))) ; theorem :: INTERVA1:31 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set "(" (Set (Var "B")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "C")) ")" )) ($#r1_interva1 :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "B")) ")" ) ($#k3_interva1 :::"_/\_"::: ) (Set "(" (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "C")) ")" ))))) ; theorem :: INTERVA1:32 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set "(" (Set (Var "B")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "C")) ")" )) ($#r1_interva1 :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "B")) ")" ) ($#k4_interva1 :::"_\/_"::: ) (Set "(" (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "C")) ")" ))))) ; theorem :: INTERVA1:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_interva1 :::"ordered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_setfam_1 :::"UNION"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: INTERVA1:34 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_interva1 :::"ordered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_setfam_1 :::"UNION"::: ) "(" (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: INTERVA1:35 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set "(" (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "B")) ")" )) ($#r1_interva1 :::"="::: ) (Set (Var "A"))))) ; theorem :: INTERVA1:36 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "B")) ")" ) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "B"))) ($#r1_interva1 :::"="::: ) (Set (Var "B"))))) ; begin theorem :: INTERVA1:37 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "U")) "holds" (Bool (Set ($#k4_setfam_1 :::"DIFFERENCE"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "U"))))) ; theorem :: INTERVA1:38 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_interva1 :::"ordered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "U")) "holds" (Bool (Set ($#k4_setfam_1 :::"DIFFERENCE"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "C")) where C "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) : (Bool "(" (Bool (Set (Set "(" ($#k7_interva1 :::"min"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k8_interva1 :::"max"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k8_interva1 :::"max"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k7_interva1 :::"min"::: ) (Set (Var "B")) ")" ))) ")" ) "}" ))) ; theorem :: INTERVA1:39 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Var "B1")) ($#r1_tarski :::"c="::: ) (Set (Var "B2")))) "holds" (Bool (Set ($#k4_setfam_1 :::"DIFFERENCE"::: ) "(" (Set "(" ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ")" ) "," (Set "(" ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "C")) where C "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) : (Bool "(" (Bool (Set (Set (Var "A1")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B2"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A2")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B1")))) ")" ) "}" ))) ; definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Const "U")); func "A" :::"_\_"::: "B" -> ($#m1_interva1 :::"IntervalSet"::: ) "of" "U" equals :: INTERVA1:def 9 (Set ($#k4_setfam_1 :::"DIFFERENCE"::: ) "(" "A" "," "B" ")" ); end; :: deftheorem defines :::"_\_"::: INTERVA1:def 9 : (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k9_interva1 :::"_\_"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_setfam_1 :::"DIFFERENCE"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )))); registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Const "U")); cluster (Set "A" ($#k9_interva1 :::"_\_"::: ) "B") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: INTERVA1:40 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k9_interva1 :::"_\_"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" (Set "(" (Set (Var "A")) ($#k5_interva1 :::"``1"::: ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "B")) ($#k6_interva1 :::"``2"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "A")) ($#k6_interva1 :::"``2"::: ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "B")) ($#k5_interva1 :::"``1"::: ) ")" ) ")" ) ")" )))) ; theorem :: INTERVA1:41 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds" (Bool (Set (Set (Var "A")) ($#k9_interva1 :::"_\_"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" (Set (Var "X")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "C")) ($#k6_interva1 :::"``2"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "Y")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "C")) ($#k5_interva1 :::"``1"::: ) ")" ) ")" ) ")" ))))) ; theorem :: INTERVA1:42 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "W")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "W")) "," (Set (Var "Z")) ")" ))) "holds" (Bool (Set (Set (Var "A")) ($#k9_interva1 :::"_\_"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" (Set (Var "X")) ($#k7_subset_1 :::"\"::: ) (Set (Var "Z")) ")" ) "," (Set "(" (Set (Var "Y")) ($#k7_subset_1 :::"\"::: ) (Set (Var "W")) ")" ) ")" ))))) ; theorem :: INTERVA1:43 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "U")) ")" ) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "U")) ")" ) ")" ) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")))) ; theorem :: INTERVA1:44 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "U")) ")" ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "U")) ")" ) ")" ) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")))) ; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set "(" ($#k2_subset_1 :::"[#]"::: ) "U" ")" ) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) "U" ")" ) ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k1_interva1 :::"Inter"::: ) "(" (Set "(" ($#k1_subset_1 :::"{}"::: ) "U" ")" ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) "U" ")" ) ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Const "U")); func "A" :::"^"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" "U" equals :: INTERVA1:def 10 (Set (Set "(" ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" ($#k2_subset_1 :::"[#]"::: ) "U" ")" ) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) "U" ")" ) ")" ")" ) ($#k9_interva1 :::"_\_"::: ) "A"); end; :: deftheorem defines :::"^"::: INTERVA1:def 10 : (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k10_interva1 :::"^"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "U")) ")" ) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "U")) ")" ) ")" ")" ) ($#k9_interva1 :::"_\_"::: ) (Set (Var "A")))))); theorem :: INTERVA1:45 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "A")) ($#k10_interva1 :::"^"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" (Set "(" (Set (Var "A")) ($#k6_interva1 :::"``2"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "A")) ($#k5_interva1 :::"``1"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" )))) ; theorem :: INTERVA1:46 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "A")) ($#k10_interva1 :::"^"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" (Set (Var "Y")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ))))) ; theorem :: INTERVA1:47 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "U")) ")" ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "U")) ")" ) ")" ")" ) ($#k10_interva1 :::"^"::: ) ) ($#r1_interva1 :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "U")) ")" ) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "U")) ")" ) ")" ))) ; theorem :: INTERVA1:48 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "U")) ")" ) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "U")) ")" ) ")" ")" ) ($#k10_interva1 :::"^"::: ) ) ($#r1_interva1 :::"="::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "U")) ")" ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "U")) ")" ) ")" ))) ; begin theorem :: INTERVA1:49 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "st" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "A")) ")" ) ($#k10_interva1 :::"^"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "U")) ")" ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "U")) ")" ) ")" )))) ; theorem :: INTERVA1:50 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "st" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "A")) ")" ) ($#k10_interva1 :::"^"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "U")) ")" ) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "U")) ")" ) ")" )))) ; theorem :: INTERVA1:51 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "st" (Bool (Set (Set (Var "A")) ($#k9_interva1 :::"_\_"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_interva1 :::"Inter"::: ) "(" (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "U")) ")" ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "U")) ")" ) ")" )))) ; theorem :: INTERVA1:52 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k4_interva1 :::"_\/_"::: ) (Set "(" (Set (Var "A")) ($#k10_interva1 :::"^"::: ) ")" ))))) ; theorem :: INTERVA1:53 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_interva1 :::"_/\_"::: ) (Set "(" (Set (Var "A")) ($#k10_interva1 :::"^"::: ) ")" ))))) ; theorem :: INTERVA1:54 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k9_interva1 :::"_\_"::: ) (Set (Var "A")))))) ; begin definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"IntervalSets"::: "U" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: INTERVA1:def 11 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" "U") ")" )); end; :: deftheorem defines :::"IntervalSets"::: INTERVA1:def 11 : (Bool "for" (Set (Var "U")) "," (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_interva1 :::"IntervalSets"::: ) (Set (Var "U")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U"))) ")" )) ")" )); definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"InterLatt"::: "U" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"LattStr"::: ) means :: INTERVA1:def 12 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k11_interva1 :::"IntervalSets"::: ) "U")) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" "U" "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" it) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a9")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "b9")))) & (Bool (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" it) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a9")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "b9")))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"InterLatt"::: INTERVA1:def 12 : (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_interva1 :::"InterLatt"::: ) (Set (Var "U")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k11_interva1 :::"IntervalSets"::: ) (Set (Var "U")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_interva1 :::"IntervalSet"::: ) "of" (Set (Var "U")) "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "b2"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a9")) ($#k4_interva1 :::"_\/_"::: ) (Set (Var "b9")))) & (Bool (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "b2"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a9")) ($#k3_interva1 :::"_/\_"::: ) (Set (Var "b9")))) ")" )) ")" ) ")" ) ")" ))); registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_interva1 :::"InterLatt"::: ) "U") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#v10_lattices :::"Lattice-like"::: ) ; end; definitionlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); mode :::"RoughSet"::: "of" "X" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ) ($#k8_mcart_1 :::":]"::: ) ) means :: INTERVA1:def 13 (Bool verum); end; :: deftheorem defines :::"RoughSet"::: INTERVA1:def 13 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ($#k8_mcart_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X"))) "iff" (Bool verum) ")" ))); theorem :: INTERVA1:55 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k4_tarski :::"]"::: ) ))))) ; definitionlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func :::"RS"::: "A" -> ($#m2_interva1 :::"RoughSet"::: ) "of" "X" equals :: INTERVA1:def 14 (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k3_roughs_1 :::"LAp"::: ) "A" ")" ) "," (Set "(" ($#k4_roughs_1 :::"UAp"::: ) "A" ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"RS"::: INTERVA1:def 14 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k13_interva1 :::"RS"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k3_roughs_1 :::"LAp"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k4_roughs_1 :::"UAp"::: ) (Set (Var "A")) ")" ) ($#k4_tarski :::"]"::: ) )))); definitionlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); let "A" be ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Const "X")); func :::"LAp"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: INTERVA1:def 15 (Set "A" ($#k1_xtuple_0 :::"`1"::: ) ); func :::"UAp"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: INTERVA1:def 16 (Set "A" ($#k2_xtuple_0 :::"`2"::: ) ); end; :: deftheorem defines :::"LAp"::: INTERVA1:def 15 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k14_interva1 :::"LAp"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_xtuple_0 :::"`1"::: ) )))); :: deftheorem defines :::"UAp"::: INTERVA1:def 16 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k15_interva1 :::"UAp"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_xtuple_0 :::"`2"::: ) )))); definitionlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); let "A", "B" be ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Const "X")); :: original: :::"="::: redefine pred "A" :::"="::: "B" means :: INTERVA1:def 17 (Bool "(" (Bool (Set ($#k14_interva1 :::"LAp"::: ) "A") ($#r1_hidden :::"="::: ) (Set ($#k14_interva1 :::"LAp"::: ) "B")) & (Bool (Set ($#k15_interva1 :::"UAp"::: ) "A") ($#r1_hidden :::"="::: ) (Set ($#k15_interva1 :::"UAp"::: ) "B")) ")" ); end; :: deftheorem defines :::"="::: INTERVA1:def 17 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_interva1 :::"="::: ) (Set (Var "B"))) "iff" (Bool "(" (Bool (Set ($#k14_interva1 :::"LAp"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k14_interva1 :::"LAp"::: ) (Set (Var "B")))) & (Bool (Set ($#k15_interva1 :::"UAp"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k15_interva1 :::"UAp"::: ) (Set (Var "B")))) ")" ) ")" ))); definitionlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); let "A", "B" be ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Const "X")); func "A" :::"_\/_"::: "B" -> ($#m2_interva1 :::"RoughSet"::: ) "of" "X" equals :: INTERVA1:def 18 (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" ($#k14_interva1 :::"LAp"::: ) "A" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k14_interva1 :::"LAp"::: ) "B" ")" ) ")" ) "," (Set "(" (Set "(" ($#k15_interva1 :::"UAp"::: ) "A" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k15_interva1 :::"UAp"::: ) "B" ")" ) ")" ) ($#k4_tarski :::"]"::: ) ); func "A" :::"_/\_"::: "B" -> ($#m2_interva1 :::"RoughSet"::: ) "of" "X" equals :: INTERVA1:def 19 (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" ($#k14_interva1 :::"LAp"::: ) "A" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k14_interva1 :::"LAp"::: ) "B" ")" ) ")" ) "," (Set "(" (Set "(" ($#k15_interva1 :::"UAp"::: ) "A" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_interva1 :::"UAp"::: ) "B" ")" ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"_\/_"::: INTERVA1:def 18 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" ($#k14_interva1 :::"LAp"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k14_interva1 :::"LAp"::: ) (Set (Var "B")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k15_interva1 :::"UAp"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k15_interva1 :::"UAp"::: ) (Set (Var "B")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )))); :: deftheorem defines :::"_/\_"::: INTERVA1:def 19 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" ($#k14_interva1 :::"LAp"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k14_interva1 :::"LAp"::: ) (Set (Var "B")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k15_interva1 :::"UAp"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_interva1 :::"UAp"::: ) (Set (Var "B")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )))); theorem :: INTERVA1:56 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k14_interva1 :::"LAp"::: ) (Set "(" (Set (Var "A")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_interva1 :::"LAp"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k14_interva1 :::"LAp"::: ) (Set (Var "B")) ")" ))))) ; theorem :: INTERVA1:57 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k15_interva1 :::"UAp"::: ) (Set "(" (Set (Var "A")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_interva1 :::"UAp"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k15_interva1 :::"UAp"::: ) (Set (Var "B")) ")" ))))) ; theorem :: INTERVA1:58 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k14_interva1 :::"LAp"::: ) (Set "(" (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_interva1 :::"LAp"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k14_interva1 :::"LAp"::: ) (Set (Var "B")) ")" ))))) ; theorem :: INTERVA1:59 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k15_interva1 :::"UAp"::: ) (Set "(" (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_interva1 :::"UAp"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_interva1 :::"UAp"::: ) (Set (Var "B")) ")" ))))) ; theorem :: INTERVA1:60 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "A"))) ($#r2_interva1 :::"="::: ) (Set (Var "A"))))) ; theorem :: INTERVA1:61 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "A"))) ($#r2_interva1 :::"="::: ) (Set (Var "A"))))) ; theorem :: INTERVA1:62 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "B"))) ($#r2_interva1 :::"="::: ) (Set (Set (Var "B")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "A")))))) ; theorem :: INTERVA1:63 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "B"))) ($#r2_interva1 :::"="::: ) (Set (Set (Var "B")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "A")))))) ; theorem :: INTERVA1:64 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "B")) ")" ) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "C"))) ($#r2_interva1 :::"="::: ) (Set (Set (Var "A")) ($#k16_interva1 :::"_\/_"::: ) (Set "(" (Set (Var "B")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "C")) ")" ))))) ; theorem :: INTERVA1:65 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "B")) ")" ) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "C"))) ($#r2_interva1 :::"="::: ) (Set (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set "(" (Set (Var "B")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "C")) ")" ))))) ; theorem :: INTERVA1:66 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set "(" (Set (Var "B")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "C")) ")" )) ($#r2_interva1 :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "B")) ")" ) ($#k16_interva1 :::"_\/_"::: ) (Set "(" (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "C")) ")" ))))) ; theorem :: INTERVA1:67 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k16_interva1 :::"_\/_"::: ) (Set "(" (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "B")) ")" )) ($#r2_interva1 :::"="::: ) (Set (Var "A"))))) ; theorem :: INTERVA1:68 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k17_interva1 :::"_/\_"::: ) (Set "(" (Set (Var "A")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "B")) ")" )) ($#r2_interva1 :::"="::: ) (Set (Var "A"))))) ; begin definitionlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); func :::"RoughSets"::: "X" -> ($#m1_hidden :::"set"::: ) means :: INTERVA1:def 20 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m2_interva1 :::"RoughSet"::: ) "of" "X") ")" )); end; :: deftheorem defines :::"RoughSets"::: INTERVA1:def 20 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k18_interva1 :::"RoughSets"::: ) (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 (Set (Var "x")) "is" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X"))) ")" )) ")" ))); registrationlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); cluster (Set ($#k18_interva1 :::"RoughSets"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); let "R" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k18_interva1 :::"RoughSets"::: ) (Set (Const "X"))); func :::"@"::: "R" -> ($#m2_interva1 :::"RoughSet"::: ) "of" "X" equals :: INTERVA1:def 21 "R"; end; :: deftheorem defines :::"@"::: INTERVA1:def 21 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k18_interva1 :::"RoughSets"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k19_interva1 :::"@"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))))); definitionlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); let "R" be ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Const "X")); func "R" :::"@"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k18_interva1 :::"RoughSets"::: ) "X") equals :: INTERVA1:def 22 "R"; end; :: deftheorem defines :::"@"::: INTERVA1:def 22 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "R")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "R")) ($#k20_interva1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "R"))))); definitionlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); func :::"RSLattice"::: "X" -> ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"LattStr"::: ) means :: INTERVA1:def 23 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k18_interva1 :::"RoughSets"::: ) "X")) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k18_interva1 :::"RoughSets"::: ) "X") (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" "X" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B9")))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A9")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "B9")))) & (Bool (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A9")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "B9")))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"RSLattice"::: INTERVA1:def 23 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "b2")) "being" ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k21_interva1 :::"RSLattice"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k18_interva1 :::"RoughSets"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k18_interva1 :::"RoughSets"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B9")))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "b2"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A9")) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "B9")))) & (Bool (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "b2"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A9")) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "B9")))) ")" )) ")" ) ")" ) ")" ))); registrationlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); cluster (Set ($#k21_interva1 :::"RSLattice"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ; end; registrationlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); cluster (Set ($#k21_interva1 :::"RSLattice"::: ) "X") -> ($#v3_lattices :::"strict"::: ) ($#v10_lattices :::"Lattice-like"::: ) ; end; registrationlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); cluster (Set ($#k21_interva1 :::"RSLattice"::: ) "X") -> ($#v3_lattices :::"strict"::: ) ($#v11_lattices :::"distributive"::: ) ; end; definitionlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); func :::"ERS"::: "X" -> ($#m2_interva1 :::"RoughSet"::: ) "of" "X" equals :: INTERVA1:def 24 (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"ERS"::: INTERVA1:def 24 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) "holds" (Bool (Set ($#k22_interva1 :::"ERS"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ))); theorem :: INTERVA1:69 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k22_interva1 :::"ERS"::: ) (Set (Var "X")) ")" ) ($#k16_interva1 :::"_\/_"::: ) (Set (Var "A"))) ($#r2_interva1 :::"="::: ) (Set (Var "A"))))) ; definitionlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); func :::"TRS"::: "X" -> ($#m2_interva1 :::"RoughSet"::: ) "of" "X" equals :: INTERVA1:def 25 (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) "X" ")" ) "," (Set "(" ($#k2_struct_0 :::"[#]"::: ) "X" ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"TRS"::: INTERVA1:def 25 : (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) "holds" (Bool (Set ($#k23_interva1 :::"TRS"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X")) ")" ) ($#k4_tarski :::"]"::: ) ))); theorem :: INTERVA1:70 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k23_interva1 :::"TRS"::: ) (Set (Var "X")) ")" ) ($#k17_interva1 :::"_/\_"::: ) (Set (Var "A"))) ($#r2_interva1 :::"="::: ) (Set (Var "A"))))) ; registrationlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); cluster (Set ($#k21_interva1 :::"RSLattice"::: ) "X") -> ($#v3_lattices :::"strict"::: ) ($#v15_lattices :::"bounded"::: ) ; end; theorem :: INTERVA1:71 (Bool "for" (Set (Var "X")) "being" ($#l1_orders_2 :::"Tolerance_Space":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k21_interva1 :::"RSLattice"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m2_interva1 :::"RoughSet"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B9")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r3_lattices :::"[="::: ) (Set (Var "B"))) "iff" (Bool "(" (Bool (Set ($#k14_interva1 :::"LAp"::: ) (Set (Var "A9"))) ($#r1_tarski :::"c="::: ) (Set ($#k14_interva1 :::"LAp"::: ) (Set (Var "B9")))) & (Bool (Set ($#k15_interva1 :::"UAp"::: ) (Set (Var "A9"))) ($#r1_tarski :::"c="::: ) (Set ($#k15_interva1 :::"UAp"::: ) (Set (Var "B9")))) ")" ) ")" )))) ; registrationlet "X" be ($#l1_orders_2 :::"Tolerance_Space":::); cluster (Set ($#k21_interva1 :::"RSLattice"::: ) "X") -> ($#v3_lattices :::"strict"::: ) ($#v4_lattice3 :::"complete"::: ) ; end;