for X, Y being ext-real-membered set
for x being LowerBound of X
for y being LowerBound of Y holds max (x,y) is LowerBound of X /\ Y