:: MSUALG_7 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem :: MSUALG_7:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th2: :: MSUALG_7:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th3: :: MSUALG_7:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MSUALG_7:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MSUALG_7:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th6: :: MSUALG_7:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: MSUALG_7:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th8: :: MSUALG_7:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th9: :: MSUALG_7:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def1 defines complete MSUALG_7:def 1 :
theorem Th10: :: MSUALG_7:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MSUALG_7:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def2 defines /\-inheriting MSUALG_7:def 2 :
:: deftheorem Def3 defines \/-inheriting MSUALG_7:def 3 :
theorem Th12: :: MSUALG_7:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: MSUALG_7:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: MSUALG_7:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th15: :: MSUALG_7:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: MSUALG_7:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th17: :: MSUALG_7:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th18: :: MSUALG_7:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MSUALG_7:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MSUALG_7:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
definition
let r1,
r2 be
Real;
assume A1:
r1 <= r2
;
func RealSubLatt r1,
r2 -> strict Lattice means :
Def4:
:: MSUALG_7:def 4
( the
carrier of
it = [.r1,r2.] & the
L_join of
it = maxreal || [.r1,r2.] & the
L_meet of
it = minreal || [.r1,r2.] );
existence
ex b1 being strict Lattice st
( the carrier of b1 = [.r1,r2.] & the L_join of b1 = maxreal || [.r1,r2.] & the L_meet of b1 = minreal || [.r1,r2.] )
uniqueness
for b1, b2 being strict Lattice st the carrier of b1 = [.r1,r2.] & the L_join of b1 = maxreal || [.r1,r2.] & the L_meet of b1 = minreal || [.r1,r2.] & the carrier of b2 = [.r1,r2.] & the L_join of b2 = maxreal || [.r1,r2.] & the L_meet of b2 = minreal || [.r1,r2.] holds
b1 = b2
;
end;
:: deftheorem Def4 defines RealSubLatt MSUALG_7:def 4 :
theorem Th21: :: MSUALG_7:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th22: :: MSUALG_7:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MSUALG_7:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th24: :: MSUALG_7:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MSUALG_7:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 