theorem Th15: :: NOMIN_4:16

for V, A being set
for a being Element of V
for x being object
for p being SCPartialNominativePredicate of V,A holds <*(PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))),(SC_assignment ((denaming (V,A,x)),a)),p*> is SFHT of (ND (V,A))