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 )
A2: A c= A \/ B by XBOOLE_1:7;
A \/ B c= Cl (A \/ B) by PRE_TOPC:18;
then A c= Cl (A \/ B) by A2;
then A3: Int A c= Int (Cl (A \/ B)) by TOPS_1:19;
assume Int (Cl (A \/ B)) = B ; :: thesis: A c= B
hence A c= B by A1, A3, TOPS_1:23; :: thesis: verum