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

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

end;

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