theorem :: NOMIN_2:21

for v being object
for V, A being set
for p, q being SCPartialNominativePredicate of V,A holds SC_exists ((PP_or (p,q)),v) = PP_or ((SC_exists (p,v)),(SC_exists (q,v)))