let X, Y be RealNormSpace; :: thesis: ( ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism implies ( X is Reflexive iff Y is Reflexive ) )
given L being Lipschitzian LinearOperator of X,Y such that AS: L is isomorphism ; :: thesis: ( X is Reflexive iff Y is Reflexive )
ex K being Lipschitzian LinearOperator of Y,X st
( K = L " & K is isomorphism ) by AS, NORMSP_3:37;
hence ( X is Reflexive iff Y is Reflexive ) by AS, NISOM11; :: thesis: verum