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

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