let Z1, Z2 be non empty strict SubSpace of T; :: thesis: ( [#] Z1 = P & [#] Z2 = P implies Z1 = Z2 )

assume that

A3: [#] Z1 = P and

A4: [#] Z2 = P ; :: thesis: Z1 = Z2

reconsider R1 = the InternalRel of Z1, R2 = the InternalRel of Z2 as Relation of P by A3, A4;

for z being set st z in P holds

Im (R1,z) = Im (R2,z)

assume that

A3: [#] Z1 = P and

A4: [#] Z2 = P ; :: thesis: Z1 = Z2

reconsider R1 = the InternalRel of Z1, R2 = the InternalRel of Z2 as Relation of P by A3, A4;

for z being set st z in P holds

Im (R1,z) = Im (R2,z)

proof

hence
Z1 = Z2
by A3, A4, RELSET_1:31; :: thesis: verum
let z be set ; :: thesis: ( z in P implies Im (R1,z) = Im (R2,z) )

assume A5: z in P ; :: thesis: Im (R1,z) = Im (R2,z)

then reconsider z1 = z as Element of Z1 by A3;

reconsider z2 = z as Element of Z2 by A4, A5;

thus Im (R1,z) = U_FT z1

.= (Im ( the InternalRel of T,z1)) /\ the carrier of Z1 by Def2

.= U_FT z2 by A3, A4, Def2

.= Im (R2,z) ; :: thesis: verum

end;assume A5: z in P ; :: thesis: Im (R1,z) = Im (R2,z)

then reconsider z1 = z as Element of Z1 by A3;

reconsider z2 = z as Element of Z2 by A4, A5;

thus Im (R1,z) = U_FT z1

.= (Im ( the InternalRel of T,z1)) /\ the carrier of Z1 by Def2

.= U_FT z2 by A3, A4, Def2

.= Im (R2,z) ; :: thesis: verum