let X be ARS ; :: thesis: for x, y being Element of X st x =*=> y holds
x <=*=> y
let x, y be Element of X; :: thesis: ( x =*=> y implies x <=*=> y )
assume A1: x =*=> y ; :: thesis: x <=*=> y
defpred S₁[ Element of X] means x <=*=> $1;
A2: S₁[x] ;
A3: for y, z being Element of X st y ==> z & S₁[y] holds
S₁[z]

proof

let y, z be Element of X; :: thesis: ( y ==> z & S₁[y] implies S₁[z] )
assume A4: y ==> z ; :: thesis: ( not S₁[y] or S₁[z] )
assume A5: S₁[y] ; :: thesis: S₁[z]
A6: y <==> z by A4;
A7: y <=*=> z by A6, Th6;
thus S₁[z] by A5, A7, Th7; :: thesis: verum

end;

thus S₁[y] from ABSRED_0:sch 2(A1, A2, A3); :: thesis: verum