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 22 :: 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 that
A2: y in AR -below x and
A3: 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 )
A4: [y,x] in AR by A2, Th13;
A5: [z,x] in AR by A3, Th13;
consider y9 being Element of L such that
A6: [y,y9] in AR and
A7: [y9,x] in AR by A1, A4;
consider z9 being Element of L such that
A8: [z,z9] in AR and
A9: [z9,x] in AR by A1, A5;
take u = y9 "\/" z9; :: thesis: ( u in AR -below x & [y,u] in AR & [z,u] in AR )
[u,x] in AR by A7, A9, Def5;
hence u in AR -below x ; :: thesis: ( [y,u] in AR & [z,u] in AR )
A10: y <= y ;
y9 <= u by YELLOW_0:22;
hence [y,u] in AR by A6, A10, Def4; :: thesis: [z,u] in AR
A11: z <= z ;
z9 <= u by YELLOW_0:22;
hence [z,u] in AR by A8, A11, Def4; :: thesis: verum