theorem Th26: :: WAYBEL17:26

for S, T being complete Scott TopLattice
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) holds
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)