defpred S₁[ ext-real-membered non empty set ] means ( c₁ is left_end & c₁ is right_end );
A: for x being Element of ExtREAL holds S₁[{.x.}]

proof

let x be Element of ExtREAL ; :: thesis: S₁[{.x.}]
( inf {x} = x & sup {x} = x ) by Lm1, Lm2;
then ( inf {x} in {x} & sup {x} in {x} ) by TARSKI:def 1;
hence S₁[{.x.}] by Def5, Def6; :: thesis: verum

end;

B: 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 S₁[B1] ; :: thesis: ( not S₁[B2] or S₁[B1 \/ B2] )
then K: ( inf B1 in B1 & sup B1 in B1 ) by Def5, Def6;
assume S₁[B2] ; :: thesis: S₁[B1 \/ B2]
then L: ( inf B2 in B2 & sup B2 in B2 ) by Def5, Def6;
inf (B1 \/ B2) = min (inf B1),(inf B2) by Th6;
then ( inf (B1 \/ B2) = inf B1 or inf (B1 \/ B2) = inf B2 ) by XXREAL_0:15;
hence inf (B1 \/ B2) in B1 \/ B2 by K, L, 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 Th6B;
then ( sup (B1 \/ B2) = sup B1 or sup (B1 \/ B2) = sup B2 ) by XXREAL_0:16;
hence sup (B1 \/ B2) in B1 \/ B2 by K, L, XBOOLE_0:def 3; :: according to XXREAL_2:def 6 :: thesis: verum

end;

C: for B being non empty Element of Fin ExtREAL holds S₁[B] from SETWISEO:sch 3(A, B);
let X be ext-real-membered non empty set ; :: thesis: ( X is finite implies ( X is left_end & X is right_end ) )
F: X c= ExtREAL by MEMBERED:2;
assume X is finite ; :: thesis: ( X is left_end & X is right_end )
then X is non empty Element of Fin ExtREAL by F, FINSUB_1:def 5;
hence ( X is left_end & X is right_end ) by C; :: thesis: verum