let T be non empty lower TopRelStr ; :: thesis: for x being Point of T holds
( (uparrow x) ` is open & uparrow x is closed )
set BB = { ((uparrow x) ` ) where x is Element of T : verum } ;
A1: { ((uparrow x) ` ) where x is Element of T : verum } is prebasis of T by Def1;
let x be Point of T; :: thesis: ( (uparrow x) ` is open & uparrow x is closed )
reconsider a = x as Element of T ;
A2: ( (uparrow a) ` in { ((uparrow x) ` ) where x is Element of T : verum } & { ((uparrow x) ` ) where x is Element of T : verum } c= the topology of T ) by A1, CANTOR_1:def 5;
hence (uparrow x) ` in the topology of T ; :: according to PRE_TOPC:def 5 :: thesis: uparrow x is closed
thus ([#] T) \ (uparrow x) in the topology of T by A2; :: according to PRE_TOPC:def 5,PRE_TOPC:def 6 :: thesis: verum