theorem Th40: :: BCIALG_2:40

for X being BCI-algebra
for x, y being Element of X
for E being Congruence of X st [x,y] in E holds
( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) )