theorem Th2: :: BCIALG_5:2

for X being BCI-algebra
for x, y being Element of X st x <= y & y <= x holds
x = y by BCIALG_1:def 7;