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