let X be ext-real-membered non empty set ; :: thesis: ( X is finite implies ( X is left_end & X is right_end ) )

defpred S_{1}[ ext-real-membered non empty set ] means ( c_{1} is left_end & c_{1} 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_{1}[B1] & S_{1}[B2] holds

S_{1}[B1 \/ B2]
_{1}[{.x.}]
_{1}[B]
from SETWISEO:sch 3(A10, A3);

hence ( X is left_end & X is right_end ) by A2; :: thesis: verum

defpred S

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

S

proof

A10:
for x being Element of ExtREAL holds S
let B1, B2 be non empty Element of Fin ExtREAL; :: thesis: ( S_{1}[B1] & S_{1}[B2] implies S_{1}[B1 \/ B2] )

assume A4: S_{1}[B1]
; :: thesis: ( not S_{1}[B2] or S_{1}[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_{1}[B2]
; :: thesis: S_{1}[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;assume A4: S

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

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

proof

for B being non empty Element of Fin ExtREAL holds S
let x be Element of ExtREAL ; :: thesis: S_{1}[{.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_{1}[{.x.}]
by A11, Def5, Def6; :: thesis: verum

end;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

hence ( X is left_end & X is right_end ) by A2; :: thesis: verum