let X be BCI-algebra; :: thesis: 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)) )

let x, y be Element of X; :: thesis: 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)) )

let E be Congruence of X; :: thesis: ( [x,y] in E implies ( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) ) )
assume A1: [x,y] in E ; :: thesis: ( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) )
A2: field E = the carrier of X by EQREL_1:9;
then A3: E is_reflexive_in the carrier of X by RELAT_2:def 9;
then A4: [y,y] in E by RELAT_2:def 1;
E is_symmetric_in the carrier of X by ;
then [y,x] in E by ;
then [(y \ y),(x \ y)] in E by ;
then A5: [(0. X),(x \ y)] in E by BCIALG_1:def 5;
[x,x] in E by ;
then [(x \ x),(y \ x)] in E by ;
then ( 0. X in {(0. X)} & [(0. X),(y \ x)] in E ) by ;
hence ( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) ) by ; :: thesis: verum