let Y be non empty TopStruct ; :: thesis: for X1, X2 being SubSpace of Y st the carrier of X1 c= the carrier of X2 holds

X1 is SubSpace of X2

let X1, X2 be SubSpace of Y; :: thesis: ( the carrier of X1 c= the carrier of X2 implies X1 is SubSpace of X2 )

set A1 = the carrier of X1;

set A2 = the carrier of X2;

A1: the carrier of X1 = [#] X1 ;

assume A2: the carrier of X1 c= the carrier of X2 ; :: thesis: X1 is SubSpace of X2

A3: the carrier of X2 = [#] X2 ;

for P being Subset of X1 holds

( P in the topology of X1 iff ex Q being Subset of X2 st

( Q in the topology of X2 & P = Q /\ the carrier of X1 ) )

X1 is SubSpace of X2

let X1, X2 be SubSpace of Y; :: thesis: ( the carrier of X1 c= the carrier of X2 implies X1 is SubSpace of X2 )

set A1 = the carrier of X1;

set A2 = the carrier of X2;

A1: the carrier of X1 = [#] X1 ;

assume A2: the carrier of X1 c= the carrier of X2 ; :: thesis: X1 is SubSpace of X2

A3: the carrier of X2 = [#] X2 ;

for P being Subset of X1 holds

( P in the topology of X1 iff ex Q being Subset of X2 st

( Q in the topology of X2 & P = Q /\ the carrier of X1 ) )

proof

hence
X1 is SubSpace of X2
by A1, A3, A2, PRE_TOPC:def 4; :: thesis: verum
let P be Subset of X1; :: thesis: ( P in the topology of X1 iff ex Q being Subset of X2 st

( Q in the topology of X2 & P = Q /\ the carrier of X1 ) )

thus ( P in the topology of X1 implies ex Q being Subset of X2 st

( Q in the topology of X2 & P = Q /\ the carrier of X1 ) ) :: thesis: ( ex Q being Subset of X2 st

( Q in the topology of X2 & P = Q /\ the carrier of X1 ) implies P in the topology of X1 )

A7: P = Q /\ the carrier of X1 ; :: thesis: P in the topology of X1

consider R being Subset of Y such that

A8: R in the topology of Y and

A9: Q = R /\ ([#] X2) by A6, PRE_TOPC:def 4;

P = R /\ ( the carrier of X2 /\ the carrier of X1) by A7, A9, XBOOLE_1:16

.= R /\ the carrier of X1 by A2, XBOOLE_1:28 ;

hence P in the topology of X1 by A1, A8, PRE_TOPC:def 4; :: thesis: verum

end;( Q in the topology of X2 & P = Q /\ the carrier of X1 ) )

thus ( P in the topology of X1 implies ex Q being Subset of X2 st

( Q in the topology of X2 & P = Q /\ the carrier of X1 ) ) :: thesis: ( ex Q being Subset of X2 st

( Q in the topology of X2 & P = Q /\ the carrier of X1 ) implies P in the topology of X1 )

proof

given Q being Subset of X2 such that A6:
Q in the topology of X2
and
assume
P in the topology of X1
; :: thesis: ex Q being Subset of X2 st

( Q in the topology of X2 & P = Q /\ the carrier of X1 )

then consider R being Subset of Y such that

A4: R in the topology of Y and

A5: P = R /\ the carrier of X1 by A1, PRE_TOPC:def 4;

reconsider Q = R /\ the carrier of X2 as Subset of X2 by XBOOLE_1:17;

take Q ; :: thesis: ( Q in the topology of X2 & P = Q /\ the carrier of X1 )

thus Q in the topology of X2 by A3, A4, PRE_TOPC:def 4; :: thesis: P = Q /\ the carrier of X1

Q /\ the carrier of X1 = R /\ ( the carrier of X2 /\ the carrier of X1) by XBOOLE_1:16

.= R /\ the carrier of X1 by A2, XBOOLE_1:28 ;

hence P = Q /\ the carrier of X1 by A5; :: thesis: verum

end;( Q in the topology of X2 & P = Q /\ the carrier of X1 )

then consider R being Subset of Y such that

A4: R in the topology of Y and

A5: P = R /\ the carrier of X1 by A1, PRE_TOPC:def 4;

reconsider Q = R /\ the carrier of X2 as Subset of X2 by XBOOLE_1:17;

take Q ; :: thesis: ( Q in the topology of X2 & P = Q /\ the carrier of X1 )

thus Q in the topology of X2 by A3, A4, PRE_TOPC:def 4; :: thesis: P = Q /\ the carrier of X1

Q /\ the carrier of X1 = R /\ ( the carrier of X2 /\ the carrier of X1) by XBOOLE_1:16

.= R /\ the carrier of X1 by A2, XBOOLE_1:28 ;

hence P = Q /\ the carrier of X1 by A5; :: thesis: verum

A7: P = Q /\ the carrier of X1 ; :: thesis: P in the topology of X1

consider R being Subset of Y such that

A8: R in the topology of Y and

A9: Q = R /\ ([#] X2) by A6, PRE_TOPC:def 4;

P = R /\ ( the carrier of X2 /\ the carrier of X1) by A7, A9, XBOOLE_1:16

.= R /\ the carrier of X1 by A2, XBOOLE_1:28 ;

hence P in the topology of X1 by A1, A8, PRE_TOPC:def 4; :: thesis: verum