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 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;
A8: 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
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;
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;
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 A8, YELLOW_0:30; :: thesis: verum