set Y = { t where t is Element of X : t <= a } ;
A1: now :: thesis: for y1 being object st y1 in { t where t is Element of X : t <= a } holds
y1 in the carrier of X
let y1 be object ; :: 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;
a \ a = 0. X by BCIALG_1:def 5;
then a <= a ;
then a in { t where t is Element of X : t <= a } ;
hence { t where t is Element of X : t <= a } is non empty Subset of X by A1, TARSKI:def 3; :: thesis: verum