theorem Th51: :: FUNCT_4:51

for f being Function holds ~ (~ f) c= f