let V, A be set ; :: thesis: (FNDSC (V,A)) . 2 = NDSS (V,(A \/ (NDSS (V,A))))
(FNDSC (V,A)) . (1 + 1) = NDSS (V,(A \/ ((FNDSC (V,A)) . 1))) by Def3;
hence (FNDSC (V,A)) . 2 = NDSS (V,(A \/ (NDSS (V,A)))) by Th9; :: thesis: verum