let X, Y be ext-real-membered set ; :: thesis: for x being LowerBound of X
for y being LowerBound of Y holds max x,y is LowerBound of X /\ Y
let x be LowerBound of X; :: thesis: for y being LowerBound of Y holds max x,y is LowerBound of X /\ Y
let y be LowerBound of Y; :: thesis: max x,y is LowerBound of X /\ Y
let a be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( a in X /\ Y implies max x,y <= a )
assume a in X /\ Y ; :: thesis: max x,y <= a
then ( a in X & a in Y ) by XBOOLE_0:def 4;
then ( x <= a & y <= a ) by Def2;
hence max x,y <= a by XXREAL_0:28; :: thesis: verum