defpred S₁[ Nat] means for Z being finite set st card Z = $1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z;
let Z be finite set ; :: thesis: ( Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) implies union Z in Z )
A1: card Z = card Z ;
A2: S₁[ 0 ] ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1] by Lm5;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence ( Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) implies union Z in Z ) by A1; :: thesis: verum