hereby :: thesis: ( P ` is open implies P is closed )

assume P is closed ; :: thesis: P ` is open
then ([#] T) \ P is open by PRE_TOPC:def 6;
hence P ` is open ; :: thesis: verum

end;

assume P ` is open ; :: thesis: P is closed
hence ([#] T) \ P is open ; :: according to PRE_TOPC:def 6 :: thesis: verum