begin
theorem Th1:
Lm1:
for S being 1-sorted
for X, Y being Subset of holds
( X c= Y ` iff Y c= X ` )
theorem Th2:
theorem Th3:
theorem
theorem Th5:
theorem
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
begin
theorem Th23:
theorem Th24:
Lm2:
for L being complete Scott TopLattice
for V being filtered Subset of
for F being Subset-Family of
for CF being Subset of st F = { (downarrow u) where u is Element of : u in V } & CF = COMPLEMENT F holds
CF is directed
theorem Th25:
theorem Th26:
:: deftheorem Def1 defines jointly_Scott-continuous WAYBEL14:def 1 :
theorem Th27:
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem
theorem Th33:
theorem
theorem
theorem
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem
theorem
theorem
theorem
theorem