let UN be Universe; :: thesis: ( NAT in UN or NAT ,UN are_equipotent )
NAT c= UN by Th16;
hence ( NAT in UN or NAT ,UN are_equipotent ) by CLASSES1:def 2; :: thesis: verum