theorem :: FUZIMPL3:25

FNegation I_RS = NegationD1