consider K being Cardinal;
{} = {} --> K ;
hence {} is Cardinal-Function ; :: thesis: verum