consider n being natural number such that
A1: X,n are_equipotent by Th74;
reconsider n = n as Element of omega by ORDINAL1:def 12;
X,n are_equipotent by A1;
hence card X is Element of omega by Def5; :: thesis: verum