set a = (0. X) \ (((0. X) \ x) \ y);
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

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;

(((0. X) \ (((0. X) \ x) \ y)) \ x) \ y = (((0. X) \ x) \ (((0. X) \ x) \ y)) \ y by BCIALG_1:7
.= ((((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