theorem :: NOMIN_3:1

for D being set
for f being BinominativeFunction of D holds f coincides_with PP_BottomPred D ;