let X be set ; :: thesis: for M being Cardinal st X c= M & card X in cf M holds
( sup X in M & union X in M )
let M be Cardinal; :: thesis: ( X c= M & card X in cf M implies ( sup X in M & union X in M ) )
assume A1: ( X c= M & card X in cf M ) ; :: thesis: ( sup X in M & union X in M )
set A = order_type_of (RelIncl X);
A2: ( sup X is_cofinal_with order_type_of (RelIncl X) & order_type_of (RelIncl X) c= M & card (order_type_of (RelIncl X)) = card X ) by A1, Th15, Th16, WELLORD2:17;
consider N being Cardinal such that
A3: ( N c= card (order_type_of (RelIncl X)) & order_type_of (RelIncl X) is_cofinal_with N & ( for C being Ordinal st order_type_of (RelIncl X) is_cofinal_with C holds
N c= C ) ) by Th18;
A4: ( N in cf M & sup X is_cofinal_with N & sup X c= sup M & sup M = M ) by A1, A2, A3, ORDINAL1:22, ORDINAL2:26, ORDINAL2:30, ORDINAL4:39;

now

assume sup X = M ; :: thesis: contradiction
then cf M c= N by A4, Def2;
hence contradiction by A1, A2, A3, CARD_1:14; :: thesis: verum

end;

then A5: sup X c< M by A4, XBOOLE_0:def 8;
hence sup X in M by ORDINAL1:21; :: thesis: union X in M
for x being set st x in X holds
x is Ordinal by A1;
then reconsider A = union X as Ordinal by ORDINAL1:35;
A c= sup X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in sup X )
assume x in A ; :: thesis: x in sup X
then consider Y being set such that
A6: ( x in Y & Y in X ) by TARSKI:def 4;
reconsider Y = Y as Ordinal by A1, A6;
Y in sup X by A6, ORDINAL2:27;
then Y c= sup X by ORDINAL1:def 2;
hence x in sup X by A6; :: thesis: verum

end;

hence union X in M by A5, ORDINAL1:21, ORDINAL1:22; :: thesis: verum