let T be up-complete Scott TopLattice; :: thesis: for x being Element of T holds Cl {x} = downarrow x

let x be Element of T; :: thesis: Cl {x} = downarrow x

downarrow x is directly_closed by Lm1;

then A1: downarrow x is closed by WAYBEL11:7;

x <= x ;

then x in downarrow x by WAYBEL_0:17;

then A2: {x} c= downarrow x by ZFMISC_1:31;

let x be Element of T; :: thesis: Cl {x} = downarrow x

downarrow x is directly_closed by Lm1;

then A1: downarrow x is closed by WAYBEL11:7;

x <= x ;

then x in downarrow x by WAYBEL_0:17;

then A2: {x} c= downarrow x by ZFMISC_1:31;

now :: thesis: for C being Subset of T st {x} c= C & C is closed holds

downarrow x c= C

hence
Cl {x} = downarrow x
by A1, A2, YELLOW_8:8; :: thesis: verumdownarrow x c= C

let C be Subset of T; :: thesis: ( {x} c= C & C is closed implies downarrow x c= C )

assume A3: {x} c= C ; :: thesis: ( C is closed implies downarrow x c= C )

reconsider D = C as Subset of T ;

assume C is closed ; :: thesis: downarrow x c= C

then A4: D is lower by WAYBEL11:7;

x in C by A3, ZFMISC_1:31;

hence downarrow x c= C by A4, WAYBEL11:6; :: thesis: verum

end;assume A3: {x} c= C ; :: thesis: ( C is closed implies downarrow x c= C )

reconsider D = C as Subset of T ;

assume C is closed ; :: thesis: downarrow x c= C

then A4: D is lower by WAYBEL11:7;

x in C by A3, ZFMISC_1:31;

hence downarrow x c= C by A4, WAYBEL11:6; :: thesis: verum