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

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;

end;

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;x <= z by A2, Def2;

hence min (x,y) <= z by A3, XXREAL_0:2; :: thesis: verum

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;y <= z by A4, Def2;

hence min (x,y) <= z by A5, XXREAL_0:2; :: thesis: verum