set S = S1 \/ S2;
thus S1 \/ S2 is finite Subset of GRZ-formula-set ; :: thesis: verum