let T be non empty TopSpace; :: thesis: for x being Element of (Omega T) holds Cl {x} = downarrow x
let x be Element of (Omega T); :: thesis: Cl {x} = downarrow x
A1: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: downarrow x c= Cl {x}
reconsider Z = {x} as Subset of T by A1;
let a be object ; :: thesis: ( a in Cl {x} implies a in downarrow x )
assume A2: a in Cl {x} ; :: thesis: a in downarrow x
then reconsider b = a as Element of (Omega T) ;
a in Cl Z by A1, A2, TOPS_3:80;
then b <= x by Def2;
hence a in downarrow x by WAYBEL_0:17; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in downarrow x or a in Cl {x} )
assume A3: a in downarrow x ; :: thesis: a in Cl {x}
then reconsider b = a as Element of (Omega T) ;
b <= x by A3, WAYBEL_0:17;
then ex Z being Subset of T st
( Z = {x} & b in Cl Z ) by Def2;
hence a in Cl {x} by A1, TOPS_3:80; :: thesis: verum