set Y = { t where t is Element of X : t <= a } ;
a \ a = 0. X by BCIALG_1:def 5;
then a <= a by BCIALG_1:def 11;
then A1: a in { t where t is Element of X : t <= a } ;

now

let y1 be set ; :: thesis: ( y1 in { t where t is Element of X : t <= a } implies y1 in the carrier of X )
assume y1 in { t where t is Element of X : t <= a } ; :: thesis: y1 in the carrier of X
then ex x1 being Element of X st
( y1 = x1 & x1 <= a ) ;
hence y1 in the carrier of X ; :: thesis: verum

end;

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