let Z1, Z2 be strict SubSpace of T; :: thesis: ( [#] Z1 = P & [#] Z2 = P implies Z1 = Z2 )
assume A3: ( [#] Z1 = P & [#] Z2 = P ) ; :: thesis: Z1 = Z2
A4: the topology of Z2 c= the topology of Z1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of Z2 or x in the topology of Z1 )
assume x in the topology of Z2 ; :: thesis: x in the topology of Z1
then ex Q being Subset of T st
( Q in the topology of T & x = Q /\ ([#] Z1) ) by A3, Def4;
hence x in the topology of Z1 by Def4; :: thesis: verum

end;

the topology of Z1 c= the topology of Z2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of Z1 or x in the topology of Z2 )
assume x in the topology of Z1 ; :: thesis: x in the topology of Z2
then ex Q being Subset of T st
( Q in the topology of T & x = Q /\ ([#] Z2) ) by A3, Def4;
hence x in the topology of Z2 by Def4; :: thesis: verum

end;

hence Z1 = Z2 by A3, A4, XBOOLE_0:def 10; :: thesis: verum