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

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

end;

hence { i where i is Element of INT : 0 <= i } is Subset of INT.Ring by TARSKI:def 3; :: thesis: verum