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 ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( a in X /\ Y implies a <= min x,y )
assume a in X /\ Y ; :: thesis: a <= min x,y
then ( a in X & a in Y ) by XBOOLE_0:def 4;
then ( a <= x & a <= y ) by Def1;
hence a <= min x,y by XXREAL_0:20; :: thesis: verum