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_{1}[ 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_{1}[u] holds

S_{1}[v]
_{1}[u] holds

S_{1}[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

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

( $1 =01=> u & u <=*= y );

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

S

proof

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

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

then B1: u =01=> v ;

given w being Element of X such that B2: ( u =01=> w & w <=*= y ) ; :: thesis: S_{1}[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_{1}[v]
by B2, B3, Lem11; :: thesis: verum

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

then B1: u =01=> v ;

given w being Element of X such that B2: ( u =01=> w & w <=*= y ) ; :: thesis: S

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

S

thus ex u being Element of X st

( x =01=> u & u <=*= y ) by A5, A2, A3; :: thesis: verum