let Z1, Z2 be non empty strict SubSpace of T; ( [#] Z1 = P & [#] Z2 = P implies Z1 = Z2 )
assume that
A3:
[#] Z1 = P
and
A4:
[#] Z2 = P
; 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
let z be
set ;
( z in P implies Im (R1,z) = Im (R2,z) )
assume A5:
z in P
;
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)
;
verum
end;
hence
Z1 = Z2
by A3, A4, RELSET_1:31; verum