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 A2, RELAT_2:def 11;

then [y,x] in E by A1, RELAT_2:def 3;

then [(y \ y),(x \ y)] in E by A4, Def9;

then A5: [(0. X),(x \ y)] in E by BCIALG_1:def 5;

[x,x] in E by A3, RELAT_2:def 1;

then [(x \ x),(y \ x)] in E by A1, Def9;

then ( 0. X in {(0. X)} & [(0. X),(y \ x)] in E ) by BCIALG_1:def 5, TARSKI:def 1;

hence ( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) ) by A5, RELAT_1:def 13; :: thesis: verum

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 A2, RELAT_2:def 11;

then [y,x] in E by A1, RELAT_2:def 3;

then [(y \ y),(x \ y)] in E by A4, Def9;

then A5: [(0. X),(x \ y)] in E by BCIALG_1:def 5;

[x,x] in E by A3, RELAT_2:def 1;

then [(x \ x),(y \ x)] in E by A1, Def9;

then ( 0. X in {(0. X)} & [(0. X),(y \ x)] in E ) by BCIALG_1:def 5, TARSKI:def 1;

hence ( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) ) by A5, RELAT_1:def 13; :: thesis: verum