for R being non empty RelStr holds
( R is well_founded iff for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H )