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 S1[ Element of X] means x >><< c1;
A4: S1[z] by A2, Lem17;
A5: for u, v being Element of X st u ==> v & S1[u] holds
S1[v]
proof
let u, v be Element of X; :: thesis: ( u ==> v & S1[u] implies S1[v] )
assume A6: u ==> v ; :: thesis: ( not S1[u] or S1[v] )
given w being Element of X such that A7: ( x =*=> w & w <=*= u ) ; :: according to ABSRED_0:def 21 :: thesis: S1[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 ;
thus S1[v] by A9, A10, DEF2; :: thesis: verum
end;
S1[y] from ABSRED_0:sch 2(A3, A4, A5);
hence x >><< y ; :: thesis: verum