set a = (0. X) \ (((0. X) \ x) \ y);

set Y = { t where t is Element of X : t \ x <= y } ;

.= ((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)) \ y by BCIALG_1:2

.= ((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)) \ (y \ (0. X)) by BCIALG_1:2

.= 0. X by BCIALG_1:1 ;

then ((0. X) \ (((0. X) \ x) \ y)) \ x <= y ;

then (0. X) \ (((0. X) \ x) \ y) in { t where t is Element of X : t \ x <= y } ;

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

set Y = { t where t is Element of X : t \ x <= y } ;

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

y1 in the carrier of X

(((0. X) \ (((0. X) \ x) \ y)) \ x) \ y =
(((0. X) \ x) \ (((0. X) \ x) \ y)) \ y
by BCIALG_1:7
y1 in the carrier of X

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

assume y1 in { t where t is Element of X : t \ x <= y } ; :: thesis: y1 in the carrier of X

then ex x1 being Element of X st

( y1 = x1 & x1 \ x <= y ) ;

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

end;assume y1 in { t where t is Element of X : t \ x <= y } ; :: thesis: y1 in the carrier of X

then ex x1 being Element of X st

( y1 = x1 & x1 \ x <= y ) ;

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

.= ((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)) \ y by BCIALG_1:2

.= ((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)) \ (y \ (0. X)) by BCIALG_1:2

.= 0. X by BCIALG_1:1 ;

then ((0. X) \ (((0. X) \ x) \ y)) \ x <= y ;

then (0. X) \ (((0. X) \ x) \ y) in { t where t is Element of X : t \ x <= y } ;

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