let X be Subset of REAL; :: thesis: ( ( not X is empty & X is closed_interval ) iff ex a, b being Real st
( a <= b & X = [.a,b.] ) )
thus ( not X is empty & X is closed_interval implies ex a, b being Real st
( a <= b & X = [.a,b.] ) ) :: thesis: ( ex a, b being Real st
( a <= b & X = [.a,b.] ) implies ( not X is empty & X is closed_interval ) )

proof

assume X: not X is empty ; :: thesis: ( not X is closed_interval or ex a, b being Real st
( a <= b & X = [.a,b.] ) )
assume X is closed_interval ; :: thesis: ex a, b being Real st
( a <= b & X = [.a,b.] )
then consider a, b being real number such that
Z: X = [.a,b.] by Def6;
reconsider a = a, b = b as Real by XREAL_0:def 1;
take a ; :: thesis: ex b being Real st
( a <= b & X = [.a,b.] )
take b ; :: thesis: ( a <= b & X = [.a,b.] )
thus a <= b by X, Z, XXREAL_1:29; :: thesis: X = [.a,b.]
thus X = [.a,b.] by Z; :: thesis: verum

end;

thus ( ex a, b being Real st
( a <= b & X = [.a,b.] ) implies ( not X is empty & X is closed_interval ) ) by Def6, XXREAL_1:30; :: thesis: verum