let T be non empty TopSpace-like reflexive transitive lower TopRelStr ; :: thesis: for x being Point of T holds Cl {x} = uparrow x
let x be Point of T; :: thesis: Cl {x} = uparrow x
reconsider y = x as Element of T ;
y <= y ;
then x in uparrow x by WAYBEL_0:18;
then {x} c= uparrow x by ZFMISC_1:31;
hence Cl {x} c= uparrow x by Th4, TOPS_1:5; :: according to XBOOLE_0:def 10 :: thesis: uparrow x c= Cl {x}
Cl {x} is upper by Th6;
then A1: uparrow (Cl {x}) c= Cl {x} by WAYBEL_0:24;
uparrow {x} c= uparrow (Cl {x}) by PRE_TOPC:18, YELLOW_3:7;
hence uparrow x c= Cl {x} by A1; :: thesis: verum