let X be BCI-algebra; :: thesis: for x, y being Element of X st x <= y & y <= x holds
x = y
let x, y be Element of X; :: thesis: ( x <= y & y <= x implies x = y )
assume ( x <= y & y <= x ) ; :: thesis: x = y
then ( x \ y = 0. X & y \ x = 0. X ) by BCIALG_1:def 11;
hence x = y by BCIALG_1:def 7; :: thesis: verum