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