set Y = { x where x is Element of X : a <= x } ;
A1: a in { x where x is Element of X : a <= x }

proof

a \ a = 0. X by Def5;
then a <= a by Def11;
hence a in { x where x is Element of X : a <= x } ; :: thesis: verum

end;

now

let y be set ; :: thesis: ( y in { x where x is Element of X : a <= x } implies y in the carrier of X )
assume y in { x where x is Element of X : a <= x } ; :: thesis: y in the carrier of X
then consider x being Element of X such that
A2: ( y = x & a <= x ) ;
thus y in the carrier of X by A2; :: thesis: verum

end;

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