let X be ARS ; :: thesis: for x, y, z being Element of X st X is DIAMOND & x <=01= y & y =*=> z holds

ex u being Element of X st

( x =*=> u & u <=01= z )

let x, y, z be Element of X; :: thesis: ( X is DIAMOND & x <=01= y & y =*=> z implies ex u being Element of X st

( x =*=> u & u <=01= z ) )

assume ( X is DIAMOND & x <=01= y & y =*=> z ) ; :: thesis: ex u being Element of X st

( x =*=> u & u <=01= z )

then ex u being Element of X st

( z =01=> u & u <=*= x ) by LemA;

hence ex u being Element of X st

( x =*=> u & u <=01= z ) ; :: thesis: verum

ex u being Element of X st

( x =*=> u & u <=01= z )

let x, y, z be Element of X; :: thesis: ( X is DIAMOND & x <=01= y & y =*=> z implies ex u being Element of X st

( x =*=> u & u <=01= z ) )

assume ( X is DIAMOND & x <=01= y & y =*=> z ) ; :: thesis: ex u being Element of X st

( x =*=> u & u <=01= z )

then ex u being Element of X st

( z =01=> u & u <=*= x ) by LemA;

hence ex u being Element of X st

( x =*=> u & u <=01= z ) ; :: thesis: verum