let X be ARS ; :: thesis: ( X is DIAMOND implies X is CONF )
assume A1: X is DIAMOND ; :: thesis: X is CONF
let x be Element of X; :: according to ABSRED_0:def 25 :: thesis: for y being Element of X st x <<>> y holds
x >><< y
let y be Element of X; :: thesis: ( x <<>> y implies x >><< y )
given z being Element of X such that A2: x <=*= z and
A3: z =*=> y ; :: according to ABSRED_0:def 20 :: thesis: x >><< y
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]

proof

let u, v be Element of X; :: thesis: ( u ==> v & S₁[u] implies S₁[v] )
assume A6: u ==> v ; :: thesis: ( not S₁[u] or S₁[v] )
given w being Element of X such that A7: ( x =*=> w & w <=*= u ) ; :: according to ABSRED_0:def 21 :: thesis: S₁[v]
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: verum

end;

S₁[y] from ABSRED_0:sch 2(A3, A4, A5);
hence x >><< y ; :: thesis: verum