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 F_Real such that
A: ( o = x & 0 <= x ) ;
thus o in the carrier of F_Real by A; :: thesis: verum

end;

hence { r where r is Element of REAL : 0 <= r } is Subset of F_Real by TARSKI:def 3; :: thesis: verum