REAL c= the carrier of R^1 by TOPMETR:17;
then reconsider P = REAL as non empty Subset of R^1 ;
take P ; :: thesis: ( not P is empty & P is interval )
thus not P is empty ; :: thesis: P is interval
let a, b be ext-real number ; :: according to XXREAL_2:def 12 :: thesis: ( not a in P or not b in P or K58(a,b) c= P )
assume ( a in P & b in P ) ; :: thesis: K58(a,b) c= P
then reconsider a = a, b = b as Real ;
[.a,b.] c= P ;
hence K58(a,b) c= P ; :: thesis: verum