set Y = { t where t is Element of X : t <= a } ;

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

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

a \ a = 0. X
by BCIALG_1:def 5;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;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

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