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 S₁[ 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 & S₁[u] holds
S₁[v]

proof

let u, v be Element of X; :: thesis: ( u ==> v & S₁[u] implies S₁[v] )
assume u ==> v ; :: thesis: ( not S₁[u] or S₁[v] )
then B1: u =01=> v ;
given w being Element of X such that B2: ( u =01=> w & w <=*= y ) ; :: thesis: S₁[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 S₁[v] by B2, B3, Lem11; :: thesis: verum

end;

A5: for u, v being Element of X st u =*=> v & S₁[u] holds
S₁[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