let T be TopSpace; :: thesis: for A, B being Subset of T st A is open & Int (Cl (A \/ B)) = B holds
A c= B
let A, B be Subset of T; :: thesis: ( A is open & Int (Cl (A \/ B)) = B implies A c= B )
assume A1: A is open ; :: thesis: ( not Int (Cl (A \/ B)) = B or A c= B )
assume A2: Int (Cl (A \/ B)) = B ; :: thesis: A c= B
( A \/ B c= Cl (A \/ B) & A c= A \/ B ) by PRE_TOPC:48, XBOOLE_1:7;
then A c= Cl (A \/ B) by XBOOLE_1:1;
then Int A c= Int (Cl (A \/ B)) by TOPS_1:48;
hence A c= B by A1, A2, TOPS_1:55; :: thesis: verum