theorem Sumrd (A B: set) (G: wff) (b: nat): $ G -> b e. B $ > $ G -> b1 b e. Sum A B $;
b1 b e. Sum A B <-> b e. B
G -> b e. B
G -> b1 b e. Sum A B