set H = H1 \/ H2;
set sq1 = [H1,phi];
set sq = [(H1 \/ H2),phi];
set R = R#1 S;
consider m being Nat such that
A1: m1 = m + 1 by NAT_1:6;
defpred S1[ Nat] means [(H1 \/ H2),phi] is m1 + 1,{[H1,phi]},{(R#1 S)} -derivable ;
A2: [((H1 \/ H2) \/ (H1 \/ H2)),phi] is 1,{[(H1 \/ H2),phi]},{(R#1 S)} -derivable ;
A3: S1[ 0 ] ;
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; :: thesis: S1[n + 1]
then [(H1 \/ H2),phi] is (n + 1) + 1,{[H1,phi]},{(R#1 S)} \/ {(R#1 S)} -derivable by Lm22, A2;
hence S1[n + 1] ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A3, A4);
 hence for b1 being object st b1 = [((H1 \/ H2) null m1),phi] holds
b1 is m1,{[H1,phi]},{(R#1 S)} -derivable by A1; :: thesis: verum