theorem Sumld (A B: set) (G: wff) (a: nat): $ G -> a e. A $ > $ G -> b0 a e. Sum A B $;
b0 a e. Sum A B <-> a e. A
G -> a e. A
G -> b0 a e. Sum A B