theorem FNegI3: :: FUZIMPL4:25

FNegation I_I3 = NegationD1