let S, T be complete Scott TopLattice; :: thesis: 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
let f be Function of S,T; :: thesis: ( ( for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T ) implies for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T )
assume A1: for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T ; :: thesis: for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T
then A2: f is monotone by Th25;
let x be Element of S; :: thesis: f . x = "\/" { (f . w) where w is Element of S : w << x } ,T
A3: f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T by A1;
set FW = { (f . w) where w is Element of S : ( w <= x & w is compact ) } ;
set FX = { (f . w) where w is Element of S : w << x } ;
set fx = f . x;
A4: { (f . w) where w is Element of S : ( w <= x & w is compact ) } c= { (f . w) where w is Element of S : w << x }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (f . w) where w is Element of S : ( w <= x & w is compact ) } or a in { (f . w) where w is Element of S : w << x } )
assume a in { (f . w) where w is Element of S : ( w <= x & w is compact ) } ; :: thesis: a in { (f . w) where w is Element of S : w << x }
then consider w being Element of S such that
A5: ( a = f . w & w <= x & w is compact ) ;
w << w by A5, WAYBEL_3:def 2;
then w << x by A5, WAYBEL_3:2;
hence a in { (f . w) where w is Element of S : w << x } by A5; :: thesis: verum

end;

A6: f . x is_>=_than { (f . w) where w is Element of S : w << x }

proof

let b be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not b in { (f . w) where w is Element of S : w << x } or b <= f . x )
assume b in { (f . w) where w is Element of S : w << x } ; :: thesis: b <= f . x
then consider ww being Element of S such that
A7: ( b = f . ww & ww << x ) ;
ww <= x by A7, WAYBEL_3:1;
hence b <= f . x by A2, A7, WAYBEL_1:def 2; :: thesis: verum

end;

for b being Element of T st b is_>=_than { (f . w) where w is Element of S : w << x } holds
f . x <= b

proof

let b be Element of T; :: thesis: ( b is_>=_than { (f . w) where w is Element of S : w << x } implies f . x <= b )
assume b is_>=_than { (f . w) where w is Element of S : w << x } ; :: thesis: f . x <= b
then b is_>=_than { (f . w) where w is Element of S : ( w <= x & w is compact ) } by A4, YELLOW_0:9;
hence f . x <= b by A3, YELLOW_0:32; :: thesis: verum

end;

hence f . x = "\/" { (f . w) where w is Element of S : w << x } ,T by A6, YELLOW_0:30; :: thesis: verum