begin
:: deftheorem Def1 defines lower WAYBEL19:def 1 :
theorem Th1:
theorem Th2:
:: deftheorem Def2 defines omega WAYBEL19:def 2 :
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
theorem Th14:
theorem Th15:
theorem
theorem
begin
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
begin
:: deftheorem Def3 defines Lawson WAYBEL19:def 3 :
theorem Th29:
theorem Th30:
theorem
theorem
:: deftheorem Def4 defines lambda WAYBEL19:def 4 :
theorem Th33:
theorem
Lm2:
for T being LATTICE
for F being Subset-Family of st ( for A being Subset of st A in F holds
A is property(S) ) holds
union F is property(S)
Lm3:
for T being LATTICE
for A1, A2 being Subset of st A1 is property(S) & A2 is property(S) holds
A1 /\ A2 is property(S)
Lm4:
for T being LATTICE holds [#] T is property(S)
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem
theorem
theorem