let A be non empty finite Subset of NAT; :: thesis: ( union A in A & ( for a being set holds
( not a in A or a in union A or a = union A ) ) )

consider a being Ordinal such that
A1: RelIncl A, RelIncl a are_isomorphic by ;
consider F1 being Function such that
A2: F1 is_isomorphism_of RelIncl A, RelIncl a by ;
A3: dom F1 = field () by ;
then dom F1 = A by WELLORD2:def 1;
then consider b being object such that
A4: b in dom F1 by XBOOLE_0:def 1;
rng F1 is finite by ;
then field () is finite by ;
then A5: a is finite by WELLORD2:def 1;
F1 . b in rng F1 by ;
then not field () is empty by ;
then not a is empty by WELLORD2:def 1;
then A6: {} in a by ;
A7: now :: thesis: not a is limit_ordinal end;
RelIncl a, RelIncl A are_isomorphic by ;
then consider F being Function such that
A8: F is_isomorphism_of RelIncl a, RelIncl A by WELLORD1:def 8;
A9: for m, n being Nat st m in dom F & n in dom F & n < m holds
F . n in F . m
proof
let m, n be Nat; :: thesis: ( m in dom F & n in dom F & n < m implies F . n in F . m )
assume that
A10: m in dom F and
A11: n in dom F and
A12: n < m ; :: thesis: F . n in F . m
F . n in rng F by ;
then F . n in field () by ;
then A13: F . n in A by WELLORD2:def 1;
then reconsider b = F . n as Nat ;
n in field () by ;
then A14: n in a by WELLORD2:def 1;
F . m in rng F by ;
then F . m in field () by ;
then A15: F . m in A by WELLORD2:def 1;
then reconsider c = F . m as Nat ;
n in { i where i is Nat : i < m } by A12;
then n in m by AXIOMS:4;
then A16: n c= m by ORDINAL1:def 2;
m in field () by ;
then m in a by WELLORD2:def 1;
then [n,m] in RelIncl a by ;
then [(F . n),(F . m)] in RelIncl A by ;
then A17: F . n c= F . m by ;
F is one-to-one by ;
then F . n <> F . m by ;
then F . n c< F . m by A17;
then b in c by ORDINAL1:11;
hence F . n in F . m ; :: thesis: verum
end;
reconsider a = a as Nat by A5;
dom F = field () by ;
then A18: dom F = a by WELLORD2:def 1;
A19: now :: thesis: for b being Ordinal st succ b = a holds
b in NAT
let b be Ordinal; :: thesis: ( succ b = a implies b in NAT )
A20: a in NAT by ORDINAL1:def 12;
assume succ b = a ; :: thesis:
then b in a by ORDINAL1:6;
hence b in NAT by ; :: thesis: verum
end;
A21: ex m being Nat st succ m = a
proof
consider b being Ordinal such that
A22: succ b = a by ;
reconsider b = b as Element of NAT by ;
take b ; :: thesis: succ b = a
thus succ b = a by A22; :: thesis: verum
end;
then consider m being Nat such that
A23: succ m = a ;
A24: rng F = field () by ;
then A25: rng F = A by WELLORD2:def 1;
then reconsider F = F as Function of a,A by ;
A26: for n, m being Nat st m in dom F & n in dom F & n < m holds
F . n in F . m by A9;
rng F = A by ;
then A27: F . () = union (rng F) by ;
A28: union a = m by ;
hence union A in A by ; :: thesis: for a being set holds
( not a in A or a in union A or a = union A )

thus for b being set holds
( not b in A or b in union A or b = union A ) :: thesis: verum
proof
let b be set ; :: thesis: ( not b in A or b in union A or b = union A )
assume A29: b in A ; :: thesis: ( b in union A or b = union A )
now :: thesis: ( not b <> union A or b in union A or b = union A )
A30: m in dom F by ;
assume A31: b <> union A ; :: thesis: ( b in union A or b = union A )
consider c being object such that
A32: c in dom F and
A33: F . c = b by ;
dom F = a by PARTFUN1:def 2;
then A34: dom F in NAT by ORDINAL1:def 12;
reconsider c = c as Element of NAT by ;
( c in m or c = m ) by ;
then c in { k where k is Nat : k < m } by ;
then ex k being Nat st
( k = c & k < m ) ;
hence ( b in union A or b = union A ) by A9, A25, A27, A28, A32, A33, A30; :: thesis: verum
end;
hence ( b in union A or b = union A ) ; :: thesis: verum
end;