let T be 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 Th8;
then A1: downarrow x is closed by Th7;
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

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 Th7;
x in C by A3, ZFMISC_1:31;
hence downarrow x c= C by A4, Th6; :: thesis: verum

end;

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