let T be TopSpace; :: thesis: for A, B being SubSpace of T st the carrier of A c= the carrier of B holds

A is SubSpace of B

let A, B be SubSpace of T; :: thesis: ( the carrier of A c= the carrier of B implies A is SubSpace of B )

assume A1: the carrier of A c= the carrier of B ; :: thesis: A is SubSpace of B

A2: for P being Subset of A holds

( P in the topology of A iff ex Q being Subset of B st

( Q in the topology of B & P = Q /\ ([#] A) ) )

hence A is SubSpace of B by A2, PRE_TOPC:def 4; :: thesis: verum

A is SubSpace of B

let A, B be SubSpace of T; :: thesis: ( the carrier of A c= the carrier of B implies A is SubSpace of B )

assume A1: the carrier of A c= the carrier of B ; :: thesis: A is SubSpace of B

A2: for P being Subset of A holds

( P in the topology of A iff ex Q being Subset of B st

( Q in the topology of B & P = Q /\ ([#] A) ) )

proof

the carrier of A c= [#] B
by A1;
let P be Subset of A; :: thesis: ( P in the topology of A iff ex Q being Subset of B st

( Q in the topology of B & P = Q /\ ([#] A) ) )

thus ( P in the topology of A implies ex Q being Subset of B st

( Q in the topology of B & P = Q /\ ([#] A) ) ) :: thesis: ( ex Q being Subset of B st

( Q in the topology of B & P = Q /\ ([#] A) ) implies P in the topology of A )

A7: P = Q /\ ([#] A) ; :: thesis: P in the topology of A

consider P9 being Subset of T such that

A8: P9 in the topology of T and

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

P = P9 /\ (([#] B) /\ ([#] A)) by A7, A9, XBOOLE_1:16

.= P9 /\ ([#] A) by A1, XBOOLE_1:28 ;

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

end;( Q in the topology of B & P = Q /\ ([#] A) ) )

thus ( P in the topology of A implies ex Q being Subset of B st

( Q in the topology of B & P = Q /\ ([#] A) ) ) :: thesis: ( ex Q being Subset of B st

( Q in the topology of B & P = Q /\ ([#] A) ) implies P in the topology of A )

proof

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

( Q in the topology of B & P = Q /\ ([#] A) )

then consider Q9 being Subset of T such that

A3: Q9 in the topology of T and

A4: P = Q9 /\ ([#] A) by PRE_TOPC:def 4;

reconsider Q = Q9 /\ ([#] B) as Subset of B ;

A5: Q in the topology of B by A3, PRE_TOPC:def 4;

P = Q9 /\ (([#] B) /\ ([#] A)) by A1, A4, XBOOLE_1:28

.= Q /\ ([#] A) by XBOOLE_1:16 ;

hence ex Q being Subset of B st

( Q in the topology of B & P = Q /\ ([#] A) ) by A5; :: thesis: verum

end;( Q in the topology of B & P = Q /\ ([#] A) )

then consider Q9 being Subset of T such that

A3: Q9 in the topology of T and

A4: P = Q9 /\ ([#] A) by PRE_TOPC:def 4;

reconsider Q = Q9 /\ ([#] B) as Subset of B ;

A5: Q in the topology of B by A3, PRE_TOPC:def 4;

P = Q9 /\ (([#] B) /\ ([#] A)) by A1, A4, XBOOLE_1:28

.= Q /\ ([#] A) by XBOOLE_1:16 ;

hence ex Q being Subset of B st

( Q in the topology of B & P = Q /\ ([#] A) ) by A5; :: thesis: verum

A7: P = Q /\ ([#] A) ; :: thesis: P in the topology of A

consider P9 being Subset of T such that

A8: P9 in the topology of T and

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

P = P9 /\ (([#] B) /\ ([#] A)) by A7, A9, XBOOLE_1:16

.= P9 /\ ([#] A) by A1, XBOOLE_1:28 ;

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

hence A is SubSpace of B by A2, PRE_TOPC:def 4; :: thesis: verum