let X be c=-linear finite set ; :: thesis: ( X is with_non-empty_elements implies card X c= card (union X) )
defpred S₁[ Nat] means for X being c=-linear finite set st X is with_non-empty_elements & card (union X) = $1 holds
card X c= card (union X);
defpred S₂[ Nat] means for n being Nat st n <= $1 holds
S₁[n];
assume A1: X is with_non-empty_elements ; :: thesis: card X c= card (union X)
A2: for m being Nat st S₂[m] holds
S₂[m + 1]

proof

let m be Nat; :: thesis: ( S₂[m] implies S₂[m + 1] )
assume A3: S₂[m] ; :: thesis: S₂[m + 1]
let n be Nat; :: thesis: ( n <= m + 1 implies S₁[n] )
assume A4: n <= m + 1 ; :: thesis: S₁[n]
let X be c=-linear finite set ; :: thesis: ( X is with_non-empty_elements & card (union X) = n implies card X c= card (union X) )
assume that
A5: X is with_non-empty_elements and
A6: card (union X) = n ; :: thesis: card X c= card (union X)
reconsider u = union X as finite set by A6;
reconsider Xu = X \ {u} as c=-linear finite set ;

per cases ( n <= m or n = m + 1 ) by A4, NAT_1:8;

suppose n <= m ; :: thesis: card X c= card (union X)

hence card X c= card (union X) by A3, A5, A6; :: thesis: verum

end;

suppose A7: n = m + 1 ; :: thesis: card X c= card (union X)

then not X is empty by A6, ZFMISC_1:2;
then A8: X = Xu \/ {u} by Th9, ZFMISC_1:116;
then u = (union Xu) \/ (union {u}) by ZFMISC_1:78
.= (union Xu) \/ u by ZFMISC_1:25 ;
then A9: union Xu c= u by XBOOLE_1:11;
then reconsider uXu = union Xu as finite set ;
uXu <> u

proof

assume A10: uXu = u ; :: thesis: contradiction
then not Xu is empty by A6, A7, ZFMISC_1:2;
then u in Xu by A10, Th9;
hence contradiction by ZFMISC_1:56; :: thesis: verum

end;

then A11: uXu c< u by A9;
then card uXu < m + 1 by A6, A7, CARD_2:48;
then card uXu <= m by NAT_1:13;
then Segm (card Xu) c= Segm (card uXu) by A3, A5;
then card Xu <= card uXu by NAT_1:39;
then card Xu < card u by A11, CARD_2:48, XXREAL_0:2;
then A12: 1 + (card Xu) <= card u by NAT_1:13;
not u in Xu by ZFMISC_1:56;
then A13: 1 + (card Xu) = card X by A8, CARD_2:41;
Segm (1 + (card Xu)) c= Segm (card u) by A12, NAT_1:39;
hence card X c= card (union X) by A13; :: thesis: verum

end;

end;

end;

A14: S₂[ 0 ]

proof

let n be Nat; :: thesis: ( n <= 0 implies S₁[n] )
assume A15: n <= 0 ; :: thesis: S₁[n]
let X be c=-linear finite set ; :: thesis: ( X is with_non-empty_elements & card (union X) = n implies card X c= card (union X) )
assume A16: ( X is with_non-empty_elements & card (union X) = n ) ; :: thesis: card X c= card (union X)
X is empty by A15, A16;
hence card X c= card (union X) ; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A14, A2);
hence card X c= card (union X) by A1; :: thesis: verum