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_{1}[ Element of X] means x >><< c_{1};

A4: S_{1}[z]
by A2, Lem17;

A5: for u, v being Element of X st u ==> v & S_{1}[u] holds

S_{1}[v]
_{1}[y]
from ABSRED_0:sch 2(A3, A4, A5);

hence x >><< y ; :: thesis: verum

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

A4: S

A5: for u, v being Element of X st u ==> v & S

S

proof

S
let u, v be Element of X; :: thesis: ( u ==> v & S_{1}[u] implies S_{1}[v] )

assume A6: u ==> v ; :: thesis: ( not S_{1}[u] or S_{1}[v] )

given w being Element of X such that A7: ( x =*=> w & w <=*= u ) ; :: according to ABSRED_0:def 21 :: thesis: S_{1}[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_{1}[v]
by A9, A10, DEF2; :: thesis: verum

end;assume A6: u ==> v ; :: thesis: ( not S

given w being Element of X such that A7: ( x =*=> w & w <=*= u ) ; :: according to ABSRED_0:def 21 :: thesis: S

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

hence x >><< y ; :: thesis: verum