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