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: 0. X in {(0. X)} by TARSKI:def 1;
( E is reflexive & E is symmetric & E is transitive & field E = the carrier of X ) by EQREL_1:16;
then ( E is_symmetric_in the carrier of X & E is_reflexive_in the carrier of X ) by RELAT_2:def 9, RELAT_2:def 11;
then ( [y,x] in E & [y,y] in E & [x,x] in E ) by A1, RELAT_2:def 1, RELAT_2:def 3;
then ( [(x \ x),(y \ x)] in E & [(y \ y),(x \ y)] in E ) by A1, Def9;
then ( [(0. X),(y \ x)] in E & [(0. X),(x \ y)] in E ) by BCIALG_1:def 5;
hence ( x \ y in Class E,(0. X) & y \ x in Class E,(0. X) ) by A2, RELAT_1:def 13; :: thesis: verum