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 ;
defpred S₁[ Element of 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;
A2: S₁[ 0 ] ;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1] by Lm5;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(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