begin
:: deftheorem defines CLweight WAYBEL31:def 1 :
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
Lm1:
for L1 being lower-bounded continuous sup-Semilattice
for T1 being Scott TopAugmentation of L1
for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2
theorem
canceled;
theorem Th14:
theorem Th15:
theorem Th16:
:: deftheorem defines Way_Up WAYBEL31:def 2 :
theorem
theorem
theorem Th19:
theorem Th20:
theorem
canceled;
theorem
canceled;
theorem
theorem Th24:
theorem Th25:
theorem Th26:
Lm2:
for L1 being lower-bounded continuous sup-Semilattice
for T being correct Lawson TopAugmentation of L1 holds weight T c= CLweight L1
theorem Th27:
theorem Th28:
Lm3:
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1 holds CLweight L1 c= weight T
theorem Th29:
theorem
theorem Th31:
theorem
theorem
theorem