let X be ext-real-membered non empty set ; :: thesis: ( X is finite implies ( X is left_end & X is right_end ) )
defpred S1[ ext-real-membered non empty set ] means ( c1 is left_end & c1 is right_end );
assume A1: X is finite ; :: thesis: ( X is left_end & X is right_end )
X c= ExtREAL by MEMBERED:2;
then A2: X is non empty Element of Fin ExtREAL by A1, FINSUB_1:def 5;
A3: for B1, B2 being non empty Element of Fin ExtREAL st S1[B1] & S1[B2] holds
S1[B1 \/ B2]
proof
let B1, B2 be non empty Element of Fin ExtREAL; :: thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] )
assume A4: S1[B1] ; :: thesis: ( not S1[B2] or S1[B1 \/ B2] )
inf (B1 \/ B2) = min ((inf B1),(inf B2)) by Th9;
then A5: ( inf (B1 \/ B2) = inf B1 or inf (B1 \/ B2) = inf B2 ) by XXREAL_0:15;
assume A6: S1[B2] ; :: thesis: S1[B1 \/ B2]
then A7: inf B2 in B2 by Def5;
inf B1 in B1 by A4, Def5;
hence inf (B1 \/ B2) in B1 \/ B2 by A7, A5, XBOOLE_0:def 3; :: according to XXREAL_2:def 5 :: thesis: B1 \/ B2 is right_end
sup (B1 \/ B2) = max ((sup B1),(sup B2)) by Th10;
then A8: ( sup (B1 \/ B2) = sup B1 or sup (B1 \/ B2) = sup B2 ) by XXREAL_0:16;
A9: sup B2 in B2 by A6, Def6;
sup B1 in B1 by A4, Def6;
hence sup (B1 \/ B2) in B1 \/ B2 by A9, A8, XBOOLE_0:def 3; :: according to XXREAL_2:def 6 :: thesis: verum
end;
A10: for x being Element of ExtREAL holds S1[{.x.}]
proof
let x be Element of ExtREAL ; :: thesis: S1[{.x.}]
sup {x} = x by Lm1;
then A11: sup {x} in {x} by TARSKI:def 1;
inf {x} = x by Lm2;
then inf {x} in {x} by TARSKI:def 1;
hence S1[{.x.}] by A11, Def5, Def6; :: thesis: verum
end;
for B being non empty Element of Fin ExtREAL holds S1[B] from SETWISEO:sch 3(A10, A3);
 hence ( X is left_end & X is right_end ) by A2; :: thesis: verum