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 ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( z in A \/ B implies min (x,y) <= z )
assume A1: z in A \/ B ; :: thesis: min (x,y) <= z
per cases ( z in A or z in B ) by A1, XBOOLE_0:def 3;
suppose A2: z in A ; :: thesis: min (x,y) <= z
A3: min (x,y) <= x by XXREAL_0:17;
x <= z by A2, Def2;
hence min (x,y) <= z by A3, XXREAL_0:2; :: thesis: verum
end;
suppose A4: z in B ; :: thesis: min (x,y) <= z
A5: min (x,y) <= y by XXREAL_0:17;
y <= z by A4, Def2;
hence min (x,y) <= z by A5, XXREAL_0:2; :: thesis: verum
end;
end;