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 } ;
let x be Point of T; :: thesis: ( (uparrow x) ` is open & uparrow x is closed )
reconsider a = x as Element of T ;
{ ((uparrow x) `) where x is Element of T : verum } is prebasis of T by Def1;
then A1: { ((uparrow x) `) where x is Element of T : verum } c= the topology of T by TOPS_2:64;
A2: (uparrow a) ` in { ((uparrow x) `) where x is Element of T : verum } ;
hence (uparrow x) ` in the topology of T by A1; :: according to PRE_TOPC:def 2 :: thesis: uparrow x is closed
thus ([#] T) \ (uparrow x) in the topology of T by A2, A1; :: according to PRE_TOPC:def 2,PRE_TOPC:def 3 :: thesis: verum