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 }

f . x <= b

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

A8:
f . x is_>=_than { (f . w) where w is Element of S : w << x }
let a be object ; :: 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 and

A6: w <= x and

A7: w is compact ;

w << w by A7;

then w << x by A6, WAYBEL_3:2;

hence a in { (f . w) where w is Element of S : w << x } by A5; :: thesis: verum

end;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 and

A6: w <= x and

A7: w is compact ;

w << w by A7;

then w << x by A6, WAYBEL_3:2;

hence a in { (f . w) where w is Element of S : w << x } by A5; :: thesis: verum

proof

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

A9: b = f . ww and

A10: ww << x ;

ww <= x by A10, WAYBEL_3:1;

hence b <= f . x by A2, A9; :: thesis: verum

end;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

A9: b = f . ww and

A10: ww << x ;

ww <= x by A10, WAYBEL_3:1;

hence b <= f . x by A2, A9; :: thesis: verum

f . x <= b

proof

hence
f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)
by A8, YELLOW_0:30; :: thesis: verum
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;

hence f . x <= b by A3, YELLOW_0:32; :: thesis: verum

end;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;

hence f . x <= b by A3, YELLOW_0:32; :: thesis: verum