defpred S₁[ Nat] means for S being non empty surreal-membered set st $1 = card S holds
ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) );
A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
let S be non empty surreal-membered set ; :: thesis: ( n + 1 = card S implies ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) ) )
assume A4: n + 1 = card S ; :: thesis: ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )
consider s being object such that
A5: s in S by XBOOLE_0:def 1;
reconsider s = s as Surreal by SURREAL0:def 16, A5;
set Ss = S \ {s};

per cases ( S \ {s} is empty or not S \ {s} is empty ) ;

suppose A6: S \ {s} is empty ; :: thesis: ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )

take s ; :: thesis: ex Max being Surreal st
( s in S & Max in S & ( for x being Surreal st x in S holds
( s <= x & x <= Max ) ) )
take s ; :: thesis: ( s in S & s in S & ( for x being Surreal st x in S holds
( s <= x & x <= s ) ) )
thus ( s in S & s in S ) by A5; :: thesis: for x being Surreal st x in S holds
( s <= x & x <= s )
let x be Surreal; :: thesis: ( x in S implies ( s <= x & x <= s ) )
assume x in S ; :: thesis: ( s <= x & x <= s )
hence ( s <= x & x <= s ) by A6, ZFMISC_1:56; :: thesis: verum

end;

suppose A7: not S \ {s} is empty ; :: thesis: ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )

card (S \ {s}) = n by A4, A5, STIRL2_1:55;
then consider Min, Max being Surreal such that
A8: ( Min in S \ {s} & Max in S \ {s} & ( for x being Surreal st x in S \ {s} holds
( Min <= x & x <= Max ) ) ) by A3, A7;
A9: Min <= Max by A8;

per cases ( Max < s or s < Min or ( Min <= s & s <= Max ) ) ;

suppose A10: Max < s ; :: thesis: ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )

take Min ; :: thesis: ex Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )
take s ; :: thesis: ( Min in S & s in S & ( for x being Surreal st x in S holds
( Min <= x & x <= s ) ) )
thus ( Min in S & s in S ) by A5, A8; :: thesis: for x being Surreal st x in S holds
( Min <= x & x <= s )
let x be Surreal; :: thesis: ( x in S implies ( Min <= x & x <= s ) )
assume x in S ; :: thesis: ( Min <= x & x <= s )

per cases then ( x in S \ {s} or x = s ) by ZFMISC_1:56;

suppose x in S \ {s} ; :: thesis: ( Min <= x & x <= s )

then ( Min <= x & x <= Max ) by A8;
hence ( Min <= x & x <= s ) by A10, Th4; :: thesis: verum

end;

suppose x = s ; :: thesis: ( Min <= x & x <= s )

hence ( Min <= x & x <= s ) by A9, A10, Th4; :: thesis: verum

end;

end;

end;

suppose A11: s < Min ; :: thesis: ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )

take s ; :: thesis: ex Max being Surreal st
( s in S & Max in S & ( for x being Surreal st x in S holds
( s <= x & x <= Max ) ) )
take Max ; :: thesis: ( s in S & Max in S & ( for x being Surreal st x in S holds
( s <= x & x <= Max ) ) )
thus ( s in S & Max in S ) by A5, A8; :: thesis: for x being Surreal st x in S holds
( s <= x & x <= Max )
let x be Surreal; :: thesis: ( x in S implies ( s <= x & x <= Max ) )
assume x in S ; :: thesis: ( s <= x & x <= Max )

per cases then ( x in S \ {s} or x = s ) by ZFMISC_1:56;

suppose x in S \ {s} ; :: thesis: ( s <= x & x <= Max )

then ( Min <= x & x <= Max ) by A8;
hence ( s <= x & x <= Max ) by A11, Th4; :: thesis: verum

end;

suppose x = s ; :: thesis: ( s <= x & x <= Max )

hence ( s <= x & x <= Max ) by A9, A11, Th4; :: thesis: verum

end;

end;

end;

suppose A12: ( Min <= s & s <= Max ) ; :: thesis: ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )

take Min ; :: thesis: ex Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )
take Max ; :: thesis: ( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )
thus ( Min in S & Max in S ) by A8; :: thesis: for x being Surreal st x in S holds
( Min <= x & x <= Max )
let x be Surreal; :: thesis: ( x in S implies ( Min <= x & x <= Max ) )
assume x in S ; :: thesis: ( Min <= x & x <= Max )
then ( x in S \ {s} or x = s ) by ZFMISC_1:56;
hence ( Min <= x & x <= Max ) by A8, A12; :: thesis: verum

end;

end;

end;

end;

end;

A13: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let S be non empty surreal-membered set ; :: thesis: ( S is finite implies ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) ) )
assume S is finite ; :: thesis: ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )
then card S is Nat ;
hence ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) ) by A13; :: thesis: verum