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