let X, Y be ext-real-membered set ; :: thesis: for x being LowerBound of X
for y being LowerBound of Y holds min x,y is LowerBound of X \/ Y
let x be LowerBound of X; :: thesis: for y being LowerBound of Y holds min x,y is LowerBound of X \/ Y
let y be LowerBound of Y; :: thesis: min 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 min x,y <= a )
assume A1: a in X \/ Y ; :: thesis: min x,y <= a

per cases ( a in X or a in Y ) by A1, XBOOLE_0:def 3;

suppose a in X ; :: thesis: min x,y <= a

then A3: x <= a by Def2;
min x,y <= x by XXREAL_0:17;
hence min x,y <= a by A3, XXREAL_0:2; :: thesis: verum

end;

suppose a in Y ; :: thesis: min x,y <= a

then A5: y <= a by Def2;
min x,y <= y by XXREAL_0:17;
hence min x,y <= a by A5, XXREAL_0:2; :: thesis: verum

end;

end;