let L be complete LATTICE; for AR being Relation of L st ( for x being Element of L holds AR -below x is_directed_wrt AR ) holds
AR is satisfying_INT
let AR be Relation of L; ( ( for x being Element of L holds AR -below x is_directed_wrt AR ) implies AR is satisfying_INT )
assume A1:
for x being Element of L holds AR -below x is_directed_wrt AR
; AR is satisfying_INT
let X, Z be Element of L; WAYBEL_4:def 21 ( [X,Z] in AR implies ex y being Element of L st
( [X,y] in AR & [y,Z] in AR ) )
assume
[X,Z] in AR
; ex y being Element of L st
( [X,y] in AR & [y,Z] in AR )
then A2:
X in AR -below Z
;
AR -below Z is_directed_wrt AR
by A1;
then consider u being Element of L such that
A3:
u in AR -below Z
and
A4:
[X,u] in AR
and
[X,u] in AR
by A2;
take
u
; ( [X,u] in AR & [u,Z] in AR )
thus
[X,u] in AR
by A4; [u,Z] in AR
thus
[u,Z] in AR
by A3, Th13; verum