for X, Y being non empty set holds card { [:X,{y}:] where y is Element of Y : verum } = card Y by Lm3;