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_{1}[ Element of X] means x <=*=> $1;

A2: S_{1}[x]
;

A3: for y, z being Element of X st y ==> z & S_{1}[y] holds

S_{1}[z]
_{1}[y]
from ABSRED_0:sch 2(A1, A2, A3); :: thesis: verum

x <=*=> y

let x, y be Element of X; :: thesis: ( x =*=> y implies x <=*=> y )

assume A1: x =*=> y ; :: thesis: x <=*=> y

defpred S

A2: S

A3: for y, z being Element of X st y ==> z & S

S

proof

thus
S
let y, z be Element of X; :: thesis: ( y ==> z & S_{1}[y] implies S_{1}[z] )

assume A4: y ==> z ; :: thesis: ( not S_{1}[y] or S_{1}[z] )

assume A5: S_{1}[y]
; :: thesis: S_{1}[z]

A6: y <==> z by A4;

A7: y <=*=> z by A6, Th6;

thus S_{1}[z]
by A5, A7, Th7; :: thesis: verum

end;assume A4: y ==> z ; :: thesis: ( not S

assume A5: S

A6: y <==> z by A4;

A7: y <=*=> z by A6, Th6;

thus S