let X, Y be ext-real-membered set ; :: thesis: for x being UpperBound of X
for y being UpperBound of Y holds min (x,y) is UpperBound of X /\ Y
let x be UpperBound of X; :: thesis: for y being UpperBound of Y holds min (x,y) is UpperBound of X /\ Y
let y be UpperBound of Y; :: thesis: min (x,y) is UpperBound of X /\ Y
let a be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( a in X /\ Y implies a <= min (x,y) )
assume A1: a in X /\ Y ; :: thesis: a <= min (x,y)
then a in Y by XBOOLE_0:def 4;
then A2: a <= y by Def1;
a in X by A1, XBOOLE_0:def 4;
then a <= x by Def1;
hence a <= min (x,y) by A2, XXREAL_0:20; :: thesis: verum