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₁[ Element of X] means ( x = $1 or 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: x =*=> y by A5, Lem2;
thus S₁[z] by A6, A4, Th4; :: thesis: verum

end;

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