let T be TopStruct ; :: thesis: for A being SubSpace of T
for B being Subset of A holds
( B is open iff ex C being Subset of T st
( C is open & C /\ ([#] A) = B ) )
let A be SubSpace of T; :: thesis: for B being Subset of A holds
( B is open iff ex C being Subset of T st
( C is open & C /\ ([#] A) = B ) )
let B be Subset of A; :: thesis: ( B is open iff ex C being Subset of T st
( C is open & C /\ ([#] A) = B ) )

hereby :: thesis: ( ex C being Subset of T st
( C is open & C /\ ([#] A) = B ) implies B is open )

assume B is open ; :: thesis: ex C being Subset of T st
( C is open & C /\ ([#] A) = B )
then B in the topology of A ;
then consider C being Subset of T such that
A1: ( C in the topology of T & C /\ ([#] A) = B ) by PRE_TOPC:def 4;
reconsider C = C as Subset of T ;
take C = C; :: thesis: ( C is open & C /\ ([#] A) = B )
thus ( C is open & C /\ ([#] A) = B ) by A1; :: thesis: verum

end;

given C being Subset of T such that A2: C is open and
A3: C /\ ([#] A) = B ; :: thesis: B is open
C in the topology of T by A2;
then B in the topology of A by A3, PRE_TOPC:def 4;
hence B is open ; :: thesis: verum