let X be c=-linear finite set ; :: thesis: ( not X is with_empty_element implies card X c= card (union X) )
defpred S₁[ Nat] means for X being c=-linear finite set st not X is with_empty_element & 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: not X is with_empty_element ; :: 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: ( not X is with_empty_element & card (union X) = n implies card X c= card (union X) )
assume that
A5: not X is with_empty_element 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:140;
then u = (union Xu) \/ (union {u}) by ZFMISC_1:96
.= (union Xu) \/ u by ZFMISC_1:31 ;
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:64; :: thesis: verum

end;

then A11: uXu c< u by A9, XBOOLE_0:def 8;
then card uXu < m + 1 by A6, A7, CARD_2:67;
then card uXu <= m by NAT_1:13;
then card Xu c= card uXu by A3, A5;
then card Xu <= card uXu by NAT_1:40;
then card Xu < card u by A11, CARD_2:67, XXREAL_0:2;
then A12: 1 + (card Xu) <= card u by NAT_1:13;
not u in Xu by ZFMISC_1:64;
then 1 + (card Xu) = card X by A8, CARD_2:54;
hence card X c= card (union X) by A12, NAT_1:40; :: thesis: verum

end;

end;

end;

A13: S₂[ 0 ]

proof

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

end;

A16: for n being Nat holds S₂[n] from NAT_1:sch 2(A13, A2);

per cases ( not union X is finite or union X is finite ) ;

suppose not union X is finite ; :: thesis: card X c= card (union X)

hence card X c= card (union X) ; :: thesis: verum

end;

suppose union X is finite ; :: thesis: card X c= card (union X)

thus card X c= card (union X) by A1, A16; :: thesis: verum

end;

end;