theorem Th1: :: WAYBEL_4:1

for L being lower-bounded sup-Semilattice
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