let L be complete LATTICE; :: thesis: for AR being auxiliary(ii) auxiliary(iii) Relation of L st AR is satisfying_INT holds
for x being Element of L holds AR -below x is_directed_wrt AR
let AR be auxiliary(ii) auxiliary(iii) Relation of L; :: thesis: ( AR is satisfying_INT implies for x being Element of L holds AR -below x is_directed_wrt AR )
assume A1: AR is satisfying_INT ; :: thesis: for x being Element of L holds AR -below x is_directed_wrt AR
let x be Element of L; :: thesis: AR -below x is_directed_wrt AR
let y be Element of L; :: according to WAYBEL_4:def 23 :: thesis: for y being Element of L st y in AR -below x & y in AR -below x holds
ex z being Element of L st
( z in AR -below x & [y,z] in AR & [y,z] in AR )
let z be Element of L; :: thesis: ( y in AR -below x & z in AR -below x implies ex z being Element of L st
( z in AR -below x & [y,z] in AR & [z,z] in AR ) )
assume ( y in AR -below x & z in AR -below x ) ; :: thesis: ex z being Element of L st
( z in AR -below x & [y,z] in AR & [z,z] in AR )
then A2: ( [y,x] in AR & [z,x] in AR ) by Th13;
then consider y' being Element of L such that
A3: ( [y,y'] in AR & [y',x] in AR ) by A1, Def22;
consider z' being Element of L such that
A4: ( [z,z'] in AR & [z',x] in AR ) by A1, A2, Def22;
take u = y' "\/" z'; :: thesis: ( u in AR -below x & [y,u] in AR & [z,u] in AR )
[u,x] in AR by A3, A4, Def6;
hence u in AR -below x ; :: thesis: ( [y,u] in AR & [z,u] in AR )
( y <= y & y' <= u ) by YELLOW_0:22;
hence [y,u] in AR by A3, Def5; :: thesis: [z,u] in AR
( z <= z & z' <= u ) by YELLOW_0:22;
hence [z,u] in AR by A4, Def5; :: thesis: verum