set R = F_Real ;
set S = { x where x is Element of REAL : 0 <= x } ;

now :: thesis: for o being object st o in { x where x is Element of REAL : 0 <= x } holds
o in the carrier of F_Real

let o be object ; :: thesis: ( o in { x where x is Element of REAL : 0 <= x } implies o in the carrier of F_Real )
assume o in { x where x is Element of REAL : 0 <= x } ; :: thesis: o in the carrier of F_Real
then consider x being Element of REAL such that
A: ( o = x & 0 <= x ) ;
thus o in the carrier of F_Real by A; :: thesis: verum

end;

then reconsider S = { x where x is Element of REAL : 0 <= x } as Subset of F_Real by TARSKI:def 3;
S is positive_cone by lemEX;
hence F_Real is ordered ; :: thesis: verum