let A, B be ext-real-membered set ; :: thesis: for x being LowerBound of A
for y being LowerBound of B holds min x,y is LowerBound of A \/ B
let x be LowerBound of A; :: thesis: for y being LowerBound of B holds min x,y is LowerBound of A \/ B
let y be LowerBound of B; :: thesis: min x,y is LowerBound of A \/ B
set m = min x,y;
let z be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( z in A \/ B implies min x,y <= z )
assume Z: z in A \/ B ; :: thesis: min x,y <= z

per cases ( z in A or z in B ) by Z, XBOOLE_0:def 3;

suppose z in A ; :: thesis: min x,y <= z

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

end;

suppose z in B ; :: thesis: min x,y <= z

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

end;

end;