set Y = { x where x is Element of X : 0. X <= x } ;

then 0. X <= 0. X ;

then 0. X in { x where x is Element of X : 0. X <= x } ;

hence { x where x is Element of X : 0. X <= x } is non empty Subset of X by A1, TARSKI:def 3; :: thesis: verum

A1: now :: thesis: for y being object st y in { x where x is Element of X : 0. X <= x } holds

y in the carrier of X

(0. X) ` = 0. X
by Def5;y in the carrier of X

let y be object ; :: thesis: ( y in { x where x is Element of X : 0. X <= x } implies y in the carrier of X )

assume y in { x where x is Element of X : 0. X <= x } ; :: thesis: y in the carrier of X

then ex x being Element of X st

( y = x & 0. X <= x ) ;

hence y in the carrier of X ; :: thesis: verum

end;assume y in { x where x is Element of X : 0. X <= x } ; :: thesis: y in the carrier of X

then ex x being Element of X st

( y = x & 0. X <= x ) ;

hence y in the carrier of X ; :: thesis: verum

then 0. X <= 0. X ;

then 0. X in { x where x is Element of X : 0. X <= x } ;

hence { x where x is Element of X : 0. X <= x } is non empty Subset of X by A1, TARSKI:def 3; :: thesis: verum