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

proof

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

end;

for r1 being real number st ( for t being real number st t in A \/ B holds
t >= r1 ) holds
min (inf A),(inf B) >= r1

proof

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

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 A4: inf A >= r1 by SEQ_4:60;

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 inf B >= r1 by SEQ_4:60;
hence min (inf A),(inf B) >= r1 by A4, XXREAL_0:20; :: thesis: verum

end;

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