let V, X be strict RealLinearSpace; ( V is Subspace of X & X is Subspace of V implies V = X )
assume that
A1:
V is Subspace of X
and
A2:
X is Subspace of V
; V = X
set VX = the carrier of X;
set VV = the carrier of V;
( the carrier of V c= the carrier of X & the carrier of X c= the carrier of V )
by A1, A2, Def2;
then A3:
the carrier of V = the carrier of X
;
set AX = the addF of X;
set AV = the addF of V;
( the addF of V = the addF of X || the carrier of V & the addF of X = the addF of V || the carrier of X )
by A1, A2, Def2;
then A4:
the addF of V = the addF of X
by A3, RELAT_1:72;
set MX = the Mult of X;
set MV = the Mult of V;
A5:
the Mult of X = the Mult of V | [:REAL, the carrier of X:]
by A2, Def2;
( 0. V = 0. X & the Mult of V = the Mult of X | [:REAL, the carrier of V:] )
by A1, Def2;
hence
V = X
by A3, A4, A5, RELAT_1:72; verum