let X be TopSpace; :: thesis: for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( B is open iff A is open )
let X0 be SubSpace of X; :: thesis: for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( B is open iff A is open )
let C, A be Subset of X; :: thesis: for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( B is open iff A is open )
let B be Subset of X0; :: thesis: ( C is open & C c= the carrier of X0 & A c= C & A = B implies ( B is open iff A is open ) )
assume that
A1: C is open and
A2: C c= the carrier of X0 and
A3: A c= C and
A4: A = B ; :: thesis: ( B is open iff A is open )
thus ( B is open implies A is open ) :: thesis: ( A is open implies B is open )

proof

assume B is open ; :: thesis: A is open
then consider F being Subset of X such that
A5: F is open and
A6: F /\ ([#] X0) = B by TOPS_2:24;
A c= F by A4, A6, XBOOLE_1:17;
then A7: A c= F /\ C by A3, XBOOLE_1:19;
F /\ C c= A by A2, A4, A6, XBOOLE_1:26;
hence A is open by A1, A5, A7, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( A is open implies B is open ) by A4, TOPS_2:25; :: thesis: verum