let X be RealBanachSpace; :: thesis: ( not X is trivial & X is Reflexive implies DualSp X is Reflexive )
assume AS: not X is trivial ; :: thesis: ( not X is Reflexive or DualSp X is Reflexive )
thus ( X is Reflexive implies DualSp X is Reflexive ) :: thesis: verum

proof

assume AS1: X is Reflexive ; :: thesis: DualSp X is Reflexive
for f being Point of (DualSp (DualSp (DualSp X))) ex h being Point of (DualSp X) st
for g being Point of (DualSp (DualSp X)) holds f . g = g . h

proof

let f be Point of (DualSp (DualSp (DualSp X))); :: thesis: ex h being Point of (DualSp X) st
for g being Point of (DualSp (DualSp X)) holds f . g = g . h
reconsider f1 = f as Lipschitzian linear-Functional of (DualSp (DualSp X)) by DUALSP01:def 10;
deffunc H₁( Element of X) -> Element of REAL = f . (BiDual $1);
P0: ex h being Function of the carrier of X,REAL st
for x being Element of X holds h . x = H₁(x) from FUNCT_2:sch 4();
consider h being Function of the carrier of X,REAL such that
P1: for x being Point of X holds h . x = f . (BiDual x) by P0;
P2: h is additive

proof

let x, y be Point of X; :: according to HAHNBAN:def 2 :: thesis: h . (x + y) = (h . x) + (h . y)
set g0 = BidualFunc X;
C2: ( BidualFunc X is additive & BidualFunc X is homogeneous ) ;
thus h . (x + y) = f . (BiDual (x + y)) by P1
.= f . ((BidualFunc X) . (x + y)) by Def2
.= f . (((BidualFunc X) . x) + ((BidualFunc X) . y)) by C2
.= (f1 . ((BidualFunc X) . x)) + (f1 . ((BidualFunc X) . y)) by HAHNBAN:def 2
.= (f . (BiDual x)) + (f . ((BidualFunc X) . y)) by Def2
.= (f . (BiDual x)) + (f . (BiDual y)) by Def2
.= (h . x) + (f . (BiDual y)) by P1
.= (h . x) + (h . y) by P1 ; :: thesis: verum

end;

P3: h is homogeneous

proof

let x be Point of X; :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds h . (b₁ * x) = b₁ * (h . x)
let r be Real; :: thesis: h . (r * x) = r * (h . x)
set g0 = BidualFunc X;
thus h . (r * x) = f . (BiDual (r * x)) by P1
.= f . ((BidualFunc X) . (r * x)) by Def2
.= f . (r * ((BidualFunc X) . x)) by LOPBAN_1:def 5
.= r * (f1 . ((BidualFunc X) . x)) by HAHNBAN:def 3
.= r * (f . (BiDual x)) by Def2
.= r * (h . x) by P1 ; :: thesis: verum

end;

for x being Point of X holds |.(h . x).| <= ||.f.|| * ||.x.||

proof

let x be Point of X; :: thesis: |.(h . x).| <= ||.f.|| * ||.x.||
set g0 = BidualFunc X;
P5: h . x = f . (BiDual x) by P1
.= f . ((BidualFunc X) . x) by Def2 ;
|.(f1 . ((BidualFunc X) . x)).| <= ||.f.|| * ||.((BidualFunc X) . x).|| by DUALSP01:26;
hence |.(h . x).| <= ||.f.|| * ||.x.|| by P5, AS, LMNORM; :: thesis: verum

end;

then h is Lipschitzian ;
then h is Point of (DualSp X) by P2, P3, DUALSP01:def 10;
then consider h being Point of (DualSp X) such that
B1: for x being Point of X holds h . x = f . (BiDual x) by P1;
B2: BidualFunc X is onto by AS1;
set g0 = BidualFunc X;
BX: for g being Point of (DualSp (DualSp X)) holds f . g = g . h

proof

let g be Point of (DualSp (DualSp X)); :: thesis: f . g = g . h
consider x being object such that
C1: ( x in dom (BidualFunc X) & g = (BidualFunc X) . x ) by B2, FUNCT_1:def 3;
reconsider x = x as Point of X by C1;
f . (BiDual x) = h . x by B1
.= (BiDual x) . h by Def1 ;
hence f . g = (BiDual x) . h by C1, Def2
.= g . h by C1, Def2 ;
:: thesis: verum

end;

take h ; :: thesis: for g being Point of (DualSp (DualSp X)) holds f . g = g . h
thus for g being Point of (DualSp (DualSp X)) holds f . g = g . h by BX; :: thesis: verum

end;

hence DualSp X is Reflexive by REFF1; :: thesis: verum

end;