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

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