let L be lower-bounded sup-Semilattice; :: thesis: for AR being auxiliary(ii) auxiliary(iii) Relation of L
for x, y, z, u being Element of L st [x,z] in AR & [y,u] in AR holds
[(x "\/" y),(z "\/" u)] in AR
let AR be auxiliary(ii) auxiliary(iii) Relation of L; :: thesis: for x, y, z, u being Element of L st [x,z] in AR & [y,u] in AR holds
[(x "\/" y),(z "\/" u)] in AR
let x, y, z, u be Element of L; :: thesis: ( [x,z] in AR & [y,u] in AR implies [(x "\/" y),(z "\/" u)] in AR )
assume that
A1: [x,z] in AR and
A2: [y,u] in AR ; :: thesis: [(x "\/" y),(z "\/" u)] in AR
A3: x <= x ;
A4: y <= y ;
A5: z <= z "\/" u by YELLOW_0:22;
A6: u <= z "\/" u by YELLOW_0:22;
A7: [x,(z "\/" u)] in AR by A1, A3, A5, Def4;
[y,(z "\/" u)] in AR by A2, A4, A6, Def4;
hence [(x "\/" y),(z "\/" u)] in AR by A7, Def5; :: thesis: verum