let L be complete LATTICE; :: thesis: for AR being auxiliary(ii) auxiliary(iii) Relation of st AR is satisfying_INT holds
for x being Element of holds AR -below x is_directed_wrt AR
let AR be auxiliary(ii) auxiliary(iii) Relation of ; :: thesis: ( AR is satisfying_INT implies for x being Element of holds AR -below x is_directed_wrt AR )
assume A1: AR is satisfying_INT ; :: thesis: for x being Element of holds AR -below x is_directed_wrt AR
let x be Element of ; :: thesis: AR -below x is_directed_wrt AR
let y be Element of ; :: according to WAYBEL_4:def 23 :: thesis: for y being Element of st y in AR -below x & y in AR -below x holds
ex z being Element of st
( z in AR -below x & [y,z] in AR & [y,z] in AR )
let z be Element of ; :: thesis: ( y in AR -below x & z in AR -below x implies ex z being Element of 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 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 y' being Element of such that
A6: [y,y'] in AR and
A7: [y',x] in AR by A1, A4, Def22;
consider z' being Element of such that
A8: [z,z'] in AR and
A9: [z',x] in AR by A1, A5, Def22;
take u = y' "\/" z'; :: thesis: ( u in AR -below x & [y,u] in AR & [z,u] in AR )
[u,x] in AR by A7, A9, Def6;
hence u in AR -below x ; :: thesis: ( [y,u] in AR & [z,u] in AR )
A10: y <= y ;
y' <= u by YELLOW_0:22;
hence [y,u] in AR by A6, A10, Def5; :: thesis: [z,u] in AR
A11: z <= z ;
z' <= u by YELLOW_0:22;
hence [z,u] in AR by A8, A11, Def5; :: thesis: verum