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 ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( a in X /\ Y implies max (x,y) <= a )
assume A1: a in X /\ Y ; :: thesis: max (x,y) <= a
then a in Y by XBOOLE_0:def 4;
then A2: y <= a by Def2;
a in X by A1, XBOOLE_0:def 4;
then x <= a by Def2;
hence max (x,y) <= a by A2, XXREAL_0:28; :: thesis: verum