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 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