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 st ( for t being Real st t in A \/ B holds
t >= r1 ) holds
min ((lower_bound A),(lower_bound B)) >= r1
proof
let r1 be Real; :: thesis: ( ( for t being Real st t in A \/ B holds
t >= r1 ) implies min ((lower_bound A),(lower_bound B)) >= r1 )
assume A3: for t being Real st t in A \/ B holds
t >= r1 ; :: thesis: min ((lower_bound A),(lower_bound B)) >= r1
now :: thesis: for t being Real st t in B holds
t >= r1
let t be Real; :: 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 Th43;
now :: thesis: for t being Real st t in A holds
t >= r1
let t be Real; :: 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 Th43;
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 st t in A \/ B holds
t >= min ((lower_bound A),(lower_bound B))
proof
let t be Real; :: 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 Def2;
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, Th44; :: thesis: verum