let X be ext-real-membered non empty set ; :: thesis: ( X is finite implies ( X is left_end & X is right_end ) )
defpred S₁[ ext-real-membered non empty set ] means ( c₁ is left_end & c₁ 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 S₁[B1] & S₁[B2] holds
S₁[B1 \/ B2]

proof

let B1, B2 be non empty Element of Fin ExtREAL; :: thesis: ( S₁[B1] & S₁[B2] implies S₁[B1 \/ B2] )
assume A4: S₁[B1] ; :: thesis: ( not S₁[B2] or S₁[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: S₁[B2] ; :: thesis: S₁[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 S₁[{.x.}]

proof

let x be Element of ExtREAL ; :: thesis: S₁[{.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 S₁[{.x.}] by A11, Def5, Def6; :: thesis: verum

end;

for B being non empty Element of Fin ExtREAL holds S₁[B] from SETWISEO:sch 3(A10, A3);
hence ( X is left_end & X is right_end ) by A2; :: thesis: verum