let A be non empty Subset of GRZ-formula-set; :: thesis: for R being GRZ-rule
for S1, S2 being GRZ-formula-finset st S1 is A,R -correct & S2 is A,R -correct holds
S1 \/ S2 is A,R -correct
let R be GRZ-rule; :: thesis: for S1, S2 being GRZ-formula-finset st S1 is A,R -correct & S2 is A,R -correct holds
S1 \/ S2 is A,R -correct
let S1, S2 be GRZ-formula-finset; :: thesis: ( S1 is A,R -correct & S2 is A,R -correct implies S1 \/ S2 is A,R -correct )
assume A1: ( S1 is A,R -correct & S2 is A,R -correct ) ; :: thesis: S1 \/ S2 is A,R -correct
consider P1, P2 being GRZ-formula-sequence such that
A3: P1 is A,R -correct and
A4: S1 = rng P1 and
A5: P2 is A,R -correct and
A6: S2 = rng P2 by A1;
reconsider S = rng (P1 ^ P2) as GRZ-formula-finset ;
S = S1 \/ S2 by A4, A6, FINSEQ_1:31;
hence S1 \/ S2 is A,R -correct by A3, A5, Th42; :: thesis: verum