let X be ARS ; :: thesis: for x, y being Element of X holds

( not x =*=> y or x = y or x =+=> y )

let x, y be Element of X; :: thesis: ( not x =*=> y or x = y or x =+=> y )

assume A1: x =*=> y ; :: thesis: ( x = y or x =+=> y )

defpred S_{1}[ Element of X] means ( x = $1 or 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

( not x =*=> y or x = y or x =+=> y )

let x, y be Element of X; :: thesis: ( not x =*=> y or x = y or x =+=> y )

assume A1: x =*=> y ; :: thesis: ( x = y or 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: x =*=> y by A5, Lem2;

thus S_{1}[z]
by A6, A4, Th4; :: thesis: verum

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

assume A5: S

A6: x =*=> y by A5, Lem2;

thus S