let X be ARS ; :: thesis: for x, y being Element of X holds
( x <==> y iff [x,y] in the reduction of X \/ ( the reduction of X ~) )
let x, y be Element of X; :: thesis: ( x <==> y iff [x,y] in the reduction of X \/ ( the reduction of X ~) )
A1: ( x ==> y iff [x,y] in the reduction of X ) ;
A2: ( x <== y iff [y,x] in the reduction of X ) ;
( [y,x] in the reduction of X iff [x,y] in the reduction of X ~ ) by RELAT_1:def 7;
hence ( x <==> y iff [x,y] in the reduction of X \/ ( the reduction of X ~) ) by A1, A2, XBOOLE_0:def 3; :: thesis: verum