let X be ARS ; :: thesis: for x, y, z being Element of X st X is DIAMOND & x <=*= z & z =01=> y holds
ex u being Element of X st
( x =01=> u & u <=*= y )
let x, y, z be Element of X; :: thesis: ( X is DIAMOND & x <=*= z & z =01=> y implies ex u being Element of X st
( x =01=> u & u <=*= y ) )
assume A1: for x, y being Element of X st x <<01>> y holds
x >>01<< y ; :: according to ABSRED_0:def 24 :: thesis: ( not x <=*= z or not z =01=> y or ex u being Element of X st
( x =01=> u & u <=*= y ) )
assume A2: x <=*= z ; :: thesis: ( not z =01=> y or ex u being Element of X st
( x =01=> u & u <=*= y ) )
assume A3: z =01=> y ; :: thesis: ex u being Element of X st
( x =01=> u & u <=*= y )
defpred S1[ Element of X] means ex u being Element of X st
( $1 =01=> u & u <=*= y );
A4: 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 u ==> v ; :: thesis: ( not S1[u] or S1[v] )
then B1: u =01=> v ;
given w being Element of X such that B2: ( u =01=> w & w <=*= y ) ; :: thesis: S1[v]
v <<01>> w by B1, B2;
then v >>01<< w by A1;
then consider u being Element of X such that
B3: ( v =01=> u & u <=01= w ) ;
thus S1[v] by B2, B3, Lem11; :: thesis: verum
end;
A5: for u, v being Element of X st u =*=> v & S1[u] holds
S1[v] from ABSRED_0:sch 1(A4);
 thus ex u being Element of X st
( x =01=> u & u <=*= y ) by A5, A2, A3; :: thesis: verum