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 & uparrow x is closed ) by Th4, ZFMISC_1:37;
hence Cl {x} c= uparrow x by TOPS_1:31; :: according to XBOOLE_0:def 10 :: thesis: uparrow x c= Cl {x}
Cl (Cl {x}) = Cl {x} ;
then Cl {x} is closed by PRE_TOPC:52;
then ( {x} c= Cl {x} & Cl {x} is upper ) by Th6, PRE_TOPC:48;
then ( uparrow {x} c= uparrow (Cl {x}) & uparrow (Cl {x}) c= Cl {x} ) by WAYBEL_0:24, YELLOW_3:7;
hence uparrow x c= Cl {x} by XBOOLE_1:1; :: thesis: verum