:: MSUALG_7  semantic presentation begin  

















theorem :: MSUALG_7:1 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k2_msualg_3 :::"id"::: )  (Set (Var "M"))) "is"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M"))))) ; 
 
theorem :: MSUALG_7:2 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "M")) "," (Set (Var "M")) ($#k6_pboole :::"|]"::: ) ) "is"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M"))))) ; 
 registrationlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "M" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); 
cluster (Set   ($#k5_msualg_5 :::"EqRelLatt"::: )  "M") ->   ($#v15_lattices :::"bounded"::: )   ; 
end; 
theorem :: MSUALG_7:3 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Var "M")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_msualg_3 :::"id"::: )  (Set (Var "M")))))) ; 
 
theorem :: MSUALG_7:4 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Var "M")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "M")) "," (Set (Var "M")) ($#k6_pboole :::"|]"::: ) )))) ; 
 
theorem :: MSUALG_7:5 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Var "M")) ")" ) "holds"  (Bool (Set (Var "X")) "is"   ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "M")) "," (Set (Var "M")) ($#k6_pboole :::"|]"::: ) ))))) ; 
 
theorem :: MSUALG_7:6 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Var "M")) ")" )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r3_lattices :::"[="::: )  (Set (Var "b"))) "iff" (Bool (Set (Var "A"))  ($#r2_pboole :::"c="::: )  (Set (Var "B")))  ")" ))))) ; 
 
theorem :: MSUALG_7:7 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Var "M")) ")" )  (Bool  "for" (Set (Var "X1")) "being"   ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "M")) "," (Set (Var "M")) ($#k6_pboole :::"|]"::: ) )  "st" (Bool (Bool (Set (Var "X1"))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "a"))  ($#r8_pboole :::"="::: )  (Set   ($#k4_mssubfam :::"meet"::: )  (Set  ($#k5_closure2 :::"|:"::: ) (Set (Var "X1")) ($#k5_closure2 :::":|"::: ) ))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "a"))  ($#r2_pboole :::"c="::: )  (Set (Var "b")))))))) ; 
 
theorem :: MSUALG_7:8 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Var "M")) ")" )  (Bool  "for" (Set (Var "X1")) "being"   ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "M")) "," (Set (Var "M")) ($#k6_pboole :::"|]"::: ) )  "st" (Bool (Bool (Set (Var "X1"))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#k4_mssubfam :::"meet"::: )  (Set  ($#k5_closure2 :::"|:"::: ) (Set (Var "X1")) ($#k5_closure2 :::":|"::: ) )) "is"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M"))))))) ; 
 definitionlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )  ; redefine attr "L" is  :::"complete":::  means :: MSUALG_7:def 1 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "L" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L" "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L"  "st" (Bool (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_lattices :::"[="::: )  (Set (Var "b")))  ")" )  ")" ))); end; 




:: deftheorem    defines :::"complete"::: MSUALG_7:def 1 :  (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v4_lattice3 :::"complete"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_lattices :::"[="::: )  (Set (Var "b")))  ")" )  ")" )))  ")" )); 
 
theorem :: MSUALG_7:9 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Var "M"))) "is"   ($#v4_lattice3 :::"complete"::: )  ))) ; 
 registrationlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "M" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); 
cluster (Set   ($#k5_msualg_5 :::"EqRelLatt"::: )  "M") ->   ($#v4_lattice3 :::"complete"::: )   ; 
end; 
theorem :: MSUALG_7:10 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Var "M")) ")" )  (Bool  "for" (Set (Var "X1")) "being"   ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "M")) "," (Set (Var "M")) ($#k6_pboole :::"|]"::: ) )  "st" (Bool (Bool (Set (Var "X1"))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_msualg_4 :::"Equivalence_Relation":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "a"))  ($#r8_pboole :::"="::: )  (Set   ($#k4_mssubfam :::"meet"::: )  (Set  ($#k5_closure2 :::"|:"::: ) (Set (Var "X1")) ($#k5_closure2 :::":|"::: ) ))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set  "("  ($#k5_msualg_5 :::"EqRelLatt"::: )  (Set (Var "M")) ")" ) ")" ))) "holds"  (Bool (Set (Var "a"))  ($#r8_pboole :::"="::: )  (Set (Var "b")))))))) ; 
 begin  definitionlet "L" be   ($#l3_lattices :::"Lattice":::); let "IT" be    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Const "L")); attr "IT" is  :::"/\-inheriting":::  means :: MSUALG_7:def 2 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "IT" "holds"  (Bool (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," "L" ")" )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "IT"))); attr "IT" is  :::"\/-inheriting":::  means :: MSUALG_7:def 3 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "IT" "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," "L" ")" )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "IT"))); end; 










:: deftheorem    defines :::"/\-inheriting"::: MSUALG_7:def 2 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "IT")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_msualg_7 :::"/\-inheriting"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "IT")) "holds"  (Bool (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "L")) ")" )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "IT")))))  ")" ))); 
 
:: deftheorem    defines :::"\/-inheriting"::: MSUALG_7:def 3 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "IT")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_msualg_7 :::"\/-inheriting"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "IT")) "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "L")) ")" )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "IT")))))  ")" ))); 
 
theorem :: MSUALG_7:11 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L9"))  "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 (Var "a"))  ($#k3_lattices :::""\/""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a9"))  ($#k3_lattices :::""\/""::: )  (Set (Var "b9")))) & (Bool (Set (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a9"))  ($#k4_lattices :::""/\""::: )  (Set (Var "b9"))))  ")" ))))) ; 
 
theorem :: MSUALG_7:12 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L9"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "a9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L9"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9")))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r3_lattice3 :::"is_less_than"::: )  (Set (Var "X"))) "iff" (Bool (Set (Var "a9"))  ($#r3_lattice3 :::"is_less_than"::: )  (Set (Var "X")))  ")" )))))) ; 
 
theorem :: MSUALG_7:13 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L9"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "a9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L9"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9")))) "holds"  (Bool  "("  (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "a"))) "iff" (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "a9")))  ")" )))))) ; 
 
theorem :: MSUALG_7:14 (Bool  "for" (Set (Var "L")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "L9")) "is"   ($#v1_msualg_7 :::"/\-inheriting"::: )  )) "holds"  (Bool (Set (Var "L9")) "is"   ($#v4_lattice3 :::"complete"::: )  ))) ; 
 
theorem :: MSUALG_7:15 (Bool  "for" (Set (Var "L")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "L9")) "is"   ($#v2_msualg_7 :::"\/-inheriting"::: )  )) "holds"  (Bool (Set (Var "L9")) "is"   ($#v4_lattice3 :::"complete"::: )  ))) ; 
 registrationlet "L" be   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_lattices :::"join-commutative"::: )     ($#v5_lattices :::"join-associative"::: )     ($#v6_lattices :::"meet-commutative"::: )     ($#v7_lattices :::"meet-associative"::: )     ($#v8_lattices :::"meet-absorbing"::: )     ($#v9_lattices :::"join-absorbing"::: )     ($#v10_lattices :::"Lattice-like"::: )     ($#v4_lattice3 :::"complete"::: )    for    ($#m2_nat_lat :::"SubLattice"::: )   "of" "L"; 
end; registrationlet "L" be   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::); 
cluster   ($#v1_msualg_7 :::"/\-inheriting"::: )    ->   ($#v4_lattice3 :::"complete"::: )    for    ($#m2_nat_lat :::"SubLattice"::: )   "of" "L"; 

cluster   ($#v2_msualg_7 :::"\/-inheriting"::: )    ->   ($#v4_lattice3 :::"complete"::: )    for    ($#m2_nat_lat :::"SubLattice"::: )   "of" "L"; 
end; 
theorem :: MSUALG_7:16 (Bool  "for" (Set (Var "L")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "L9")) "is"   ($#v1_msualg_7 :::"/\-inheriting"::: )  )) "holds"  (Bool  "for" (Set (Var "A9")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L9")) "holds"  (Bool (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "A9")) "," (Set (Var "L")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "A9")) "," (Set (Var "L9")) ")" ))))) ; 
 
theorem :: MSUALG_7:17 (Bool  "for" (Set (Var "L")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "L9")) "is"   ($#v2_msualg_7 :::"\/-inheriting"::: )  )) "holds"  (Bool  "for" (Set (Var "A9")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L9")) "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "A9")) "," (Set (Var "L")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "A9")) "," (Set (Var "L9")) ")" ))))) ; 
 
theorem :: MSUALG_7:18 (Bool  "for" (Set (Var "L")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "L9")) "is"   ($#v1_msualg_7 :::"/\-inheriting"::: )  )) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A9")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L9"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "A9")))) "holds"  (Bool (Set   ($#k16_lattice3 :::""/\""::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )  (Set (Var "A9")))))))) ; 
 
theorem :: MSUALG_7:19 (Bool  "for" (Set (Var "L")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "L9")) "is"   ($#v2_msualg_7 :::"\/-inheriting"::: )  )) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A9")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L9"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "A9")))) "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )  (Set (Var "A9")))))))) ; 
 begin  definitionlet "r1", "r2" be   ($#m1_subset_1 :::"Real":::); assume 
(Bool (Set (Const "r1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "r2")))
 ; func  :::"RealSubLatt":::  "(" "r1" "," "r2" ")"  ->   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) means :: MSUALG_7:def 4 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) "r1" "," "r2" ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_real_lat :::"maxreal"::: ) )  ($#k1_realset1 :::"||"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) "r1" "," "r2" ($#k1_rcomp_1 :::".]"::: ) ))) & (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_real_lat :::"minreal"::: ) )  ($#k1_realset1 :::"||"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) "r1" "," "r2" ($#k1_rcomp_1 :::".]"::: ) )))  ")" ); end; 







:: deftheorem    defines :::"RealSubLatt"::: MSUALG_7:def 4 :  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r2")))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_msualg_7 :::"RealSubLatt"::: )   "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_real_lat :::"maxreal"::: ) )  ($#k1_realset1 :::"||"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k1_rcomp_1 :::".]"::: ) ))) & (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_real_lat :::"minreal"::: ) )  ($#k1_realset1 :::"||"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k1_rcomp_1 :::".]"::: ) )))  ")" )  ")" ))); 
 
theorem :: MSUALG_7:20 (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r2")))) "holds"  (Bool (Set   ($#k1_msualg_7 :::"RealSubLatt"::: )   "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" ) "is"   ($#v4_lattice3 :::"complete"::: )  )) ; 
 
theorem :: MSUALG_7:21 (Bool  "ex" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set   ($#k1_msualg_7 :::"RealSubLatt"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ) "st"  (Bool  "("  (Bool (Set (Var "L9")) "is"   ($#v2_msualg_7 :::"\/-inheriting"::: )  ) & (Bool (Bool  "not" (Set (Var "L9")) "is"   ($#v1_msualg_7 :::"/\-inheriting"::: )  ))  ")" )) ; 
 
theorem :: MSUALG_7:22 (Bool  "ex" (Set (Var "L")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)(Bool  "ex" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L")) "st"  (Bool  "("  (Bool (Set (Var "L9")) "is"   ($#v2_msualg_7 :::"\/-inheriting"::: )  ) & (Bool (Bool  "not" (Set (Var "L9")) "is"   ($#v1_msualg_7 :::"/\-inheriting"::: )  ))  ")" ))) ; 
 
theorem :: MSUALG_7:23 (Bool  "ex" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set   ($#k1_msualg_7 :::"RealSubLatt"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ) "st"  (Bool  "("  (Bool (Set (Var "L9")) "is"   ($#v1_msualg_7 :::"/\-inheriting"::: )  ) & (Bool (Bool  "not" (Set (Var "L9")) "is"   ($#v2_msualg_7 :::"\/-inheriting"::: )  ))  ")" )) ; 
 
theorem :: MSUALG_7:24 (Bool  "ex" (Set (Var "L")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)(Bool  "ex" (Set (Var "L9")) "being"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set (Var "L")) "st"  (Bool  "("  (Bool (Set (Var "L9")) "is"   ($#v1_msualg_7 :::"/\-inheriting"::: )  ) & (Bool (Bool  "not" (Set (Var "L9")) "is"   ($#v2_msualg_7 :::"\/-inheriting"::: )  ))  ")" ))) ;