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

( 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