let X be TopSpace; :: thesis: for X1 being SubSpace of X
for X2 being SubSpace of X1 holds X2 is SubSpace of X
let X1 be SubSpace of X; :: thesis: for X2 being SubSpace of X1 holds X2 is SubSpace of X
let X2 be SubSpace of X1; :: thesis: X2 is SubSpace of X
A1: [#] X2 c= [#] X1 by PRE_TOPC:def 4;
[#] X1 c= [#] X by PRE_TOPC:def 4;
hence [#] X2 c= [#] X by A1, XBOOLE_1:1; :: according to PRE_TOPC:def 4 :: thesis: for b1 being Element of K10( the carrier of X2) holds
( ( not b1 in the topology of X2 or ex b2 being Element of K10( the carrier of X) st
( b2 in the topology of X & b1 = b2 /\ ([#] X2) ) ) & ( for b2 being Element of K10( the carrier of X) holds
( not b2 in the topology of X or not b1 = b2 /\ ([#] X2) ) or b1 in the topology of X2 ) )
thus for P being Subset of X2 holds
( P in the topology of X2 iff ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] X2) ) ) :: thesis: verum
proof
let P be Subset of X2; :: thesis: ( P in the topology of X2 iff ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] X2) ) )
reconsider P1 = P as Subset of X2 ;
thus ( P in the topology of X2 implies ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] X2) ) ) :: thesis: ( ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] X2) ) implies P in the topology of X2 )
proof
assume P in the topology of X2 ; :: thesis: ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] X2) )
then consider R being Subset of X1 such that
A2: R in the topology of X1 and
A3: P = R /\ ([#] X2) by PRE_TOPC:def 4;
consider Q being Subset of X such that
A4: Q in the topology of X and
A5: R = Q /\ ([#] X1) by A2, PRE_TOPC:def 4;
Q /\ ([#] X2) = Q /\ (([#] X1) /\ ([#] X2)) by A1, XBOOLE_1:28
.= P by A3, A5, XBOOLE_1:16 ;
hence ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] X2) ) by A4; :: thesis: verum
end;
given Q being Subset of X such that A6: Q in the topology of X and
A7: P = Q /\ ([#] X2) ; :: thesis: P in the topology of X2
reconsider R = Q /\ ([#] X1) as Subset of X1 ;
reconsider Q1 = Q as Subset of X ;
Q1 is open by A6;
then A8: R is open by TOPS_2:24;
R /\ ([#] X2) = Q /\ (([#] X1) /\ ([#] X2)) by XBOOLE_1:16
.= P by A1, A7, XBOOLE_1:28 ;
then P1 is open by A8, TOPS_2:24;
hence P in the topology of X2 ; :: thesis: verum
end;