let NT be NTopSpace; :: thesis: for A, B being Subset of NT st B = ([#] NT) \ A holds
( A is open iff B is closed )
let A, B be Subset of NT; :: thesis: ( B = ([#] NT) \ A implies ( A is open iff B is closed ) )
assume A1: B = ([#] NT) \ A ; :: thesis: ( A is open iff B is closed )
now :: thesis: ( ( A is open implies B is closed ) & ( B is closed implies A is open ) )
hereby :: thesis: ( B is closed implies A is open )
assume A2: A is open ; :: thesis: B is closed
([#] NT) \ B = ([#] NT) /\ A by A1, XBOOLE_1:48
.= A by XBOOLE_1:28 ;
hence B is closed by A2; :: thesis: verum
end;
hereby :: thesis: verum
assume A3: B is closed ; :: thesis: A is open
then reconsider NB = ([#] NT) \ B as Subset of NT ;
NB = ([#] NT) /\ A by A1, XBOOLE_1:48
.= A by XBOOLE_1:28 ;
hence A is open by A3; :: thesis: verum
end;
end;
hence ( A is open iff B is closed ) ; :: thesis: verum