let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; :: thesis: for x being Element of T holds Cl {x} = downarrow x
let x be Element of T; :: thesis: Cl {x} = downarrow x
reconsider T9 = T as Scott TopAugmentation of T by YELLOW_9:44;
reconsider dx = downarrow x as Subset of T9 ;
reconsider A = {x} as Subset of T9 ;
A1: downarrow x is closed by WAYBEL11:11;
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 T9 st A c= C & C is closed holds
dx c= C

let C be Subset of T9; :: thesis: ( A c= C & C is closed implies dx c= C )
assume A3: A c= C ; :: thesis: ( C is closed implies dx c= C )
reconsider D = C as Subset of T9 ;
assume C is closed ; :: thesis: dx c= C
then A4: D is lower by WAYBEL11:7;
x in C by A3, ZFMISC_1:31;
hence dx c= C by A4, WAYBEL11:6; :: thesis: verum

end;

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