consider n being Nat such that
A1: X,n are_equipotent by Lm3;
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 Def2; :: thesis: verum