begin
theorem
theorem Th2:
theorem Th3:
theorem
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def1 defines complete MSUALG_7:def 1 :
theorem Th10:
theorem
begin
:: deftheorem Def2 defines /\-inheriting MSUALG_7:def 2 :
:: deftheorem Def3 defines \/-inheriting MSUALG_7:def 3 :
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem
begin
definition
let r1,
r2 be
Real;
assume A1:
r1 <= r2
;
func RealSubLatt r1,
r2 -> strict Lattice means :
Def4:
( 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:
theorem Th22:
theorem
theorem Th24:
theorem