let X be ARS ; :: thesis:
assume A1: X is DIAMOND ; :: thesis:
let x be Element of X; :: according to ABSRED_0:def 25 :: thesis:
let y be Element of X; :: thesis:
given z being Element of X such that A2: x <=*= z and
A3: z =*=> y ; :: according to ABSRED_0:def 20 :: thesis:
defpred S₁[ Element of X] means x >><< c₁;
A4: S₁[z] by A2, Lem17;
A5: for u, v being Element of X st u ==> v & S₁[u] holds
S₁[v]

let u, v be Element of X; :: thesis:
assume A6: u ==> v ; :: thesis:
given w being Element of X such that A7: ( x =*=> w & w <=*= u ) ; :: according to ABSRED_0:def 21 :: thesis:
A8: u =01=> v by A6;
consider a being Element of X such that
A9: ( w =01=> a & a <=*= v ) by A1, A7, A8, LemA;
A10: x =*=> a by A7, A9, Lem11;
thus S₁[v] by A9, A10, DEF2; :: thesis:

end;