for TS being TopSpace
for P being Subset of TS holds
( P is open iff Fr P = (Cl P) \ P )