take {} ; :: thesis: {} is Cardinal-yielding
{} is Cardinal-yielding

proof

let x be set ; :: according to CARD_3:def 1 :: thesis: ( not x in dom {} or {} . x is set )
thus ( not x in dom {} or {} . x is set ) ; :: thesis: verum

end;

hence {} is Cardinal-yielding ; :: thesis: verum