let L be complete LATTICE; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: AR is satisfying_INT
let X, Z be Element of L; :: according to WAYBEL_4:def 21 :: thesis: ( [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 ; :: thesis: 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 ; :: thesis: ( [X,u] in AR & [u,Z] in AR )
thus [X,u] in AR by A4; :: thesis: [u,Z] in AR
thus [u,Z] in AR by A3, Th13; :: thesis: verum