let A, B be non empty bounded_below Subset of REAL ; :: thesis: lower_bound (A \/ B) = min (lower_bound A),(lower_bound B)
set r = min (lower_bound A),(lower_bound B);
A1: min (lower_bound A),(lower_bound B) <= lower_bound B by XXREAL_0:17;
A2: for r1 being real number st ( for t being real number st t in A \/ B holds
t >= r1 ) holds
min (lower_bound A),(lower_bound B) >= r1

proof

let r1 be real number ; :: thesis: ( ( for t being real number st t in A \/ B holds
t >= r1 ) implies min (lower_bound A),(lower_bound B) >= r1 )
assume A3: for t being real number st t in A \/ B holds
t >= r1 ; :: thesis: min (lower_bound A),(lower_bound B) >= r1

now

let t be real number ; :: thesis: ( t in B implies t >= r1 )
assume t in B ; :: thesis: t >= r1
then t in A \/ B by XBOOLE_0:def 3;
hence t >= r1 by A3; :: thesis: verum

end;

then A4: lower_bound B >= r1 by SEQ_4:60;

now

let t be real number ; :: thesis: ( t in A implies t >= r1 )
assume t in A ; :: thesis: t >= r1
then t in A \/ B by XBOOLE_0:def 3;
hence t >= r1 by A3; :: thesis: verum

end;

then lower_bound A >= r1 by SEQ_4:60;
hence min (lower_bound A),(lower_bound B) >= r1 by A4, XXREAL_0:20; :: thesis: verum

end;

A5: min (lower_bound A),(lower_bound B) <= lower_bound A by XXREAL_0:17;
for t being real number st t in A \/ B holds
t >= min (lower_bound A),(lower_bound B)

proof

let t be real number ; :: thesis: ( t in A \/ B implies t >= min (lower_bound A),(lower_bound B) )
assume t in A \/ B ; :: thesis: t >= min (lower_bound A),(lower_bound B)
then ( t in A or t in B ) by XBOOLE_0:def 3;
then ( lower_bound A <= t or lower_bound B <= t ) by SEQ_4:def 5;
hence t >= min (lower_bound A),(lower_bound B) by A5, A1, XXREAL_0:2; :: thesis: verum

end;

hence lower_bound (A \/ B) = min (lower_bound A),(lower_bound B) by A2, SEQ_4:61; :: thesis: verum