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 A1: ( [x,z] in AR & [y,u] in AR ) ; :: thesis: [(x "\/" y),(z "\/" u)] in AR
A2: ( x <= x & y <= y ) ;
( z <= z "\/" u & u <= z "\/" u ) by YELLOW_0:22;
then ( [x,(z "\/" u)] in AR & [y,(z "\/" u)] in AR ) by A1, A2, Def5;
hence [(x "\/" y),(z "\/" u)] in AR by Def6; :: thesis: verum