let X be RealBanachSpace; :: thesis: ( not X is trivial implies ( X is Reflexive iff DualSp X is Reflexive ) )
assume AS: not X is trivial ; :: thesis: ( X is Reflexive iff DualSp X is Reflexive )
hence ( X is Reflexive implies DualSp X is Reflexive ) by Lm77R; :: thesis: ( DualSp X is Reflexive implies X is Reflexive )
assume AS2: DualSp X is Reflexive ; :: thesis: X is Reflexive
not DualSp X is trivial by AS, Lm65A1;
then C2: DualSp (DualSp X) is Reflexive by AS2, Lm77R;
consider L being Lipschitzian LinearOperator of X,(Im (BidualFunc X)) such that
C3: L is isomorphism by AS, Th74A;
set f = BidualFunc X;
set V = DualSp (DualSp X);
D0: rng (BidualFunc X) is linearly-closed by NORMSP_3:35;
D1: rng (BidualFunc X) <> {}
proof
assume rng (BidualFunc X) = {} ; :: thesis: contradiction
then dom (BidualFunc X) = {} by RELAT_1:42;
hence contradiction by FUNCT_2:def 1; :: thesis: verum
end;
then C4: the carrier of (Im (BidualFunc X)) = rng (BidualFunc X) by NORMSP_3:31, D0;
Im (BidualFunc X) is complete by C3, NORMSP_3:44;
then rng (BidualFunc X) is closed by C4, NORMSP_3:48;
then Im (BidualFunc X) is Reflexive by C2, D0, Th76, D1;
hence X is Reflexive by C3, NISOM12; :: thesis: verum