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:54; verum