set H = H1 \/ H2;
set sq1 = [H1,phi];
set sq = [(H1 \/ H2),phi];
consider m being Nat such that
B3: m1 = m + 1 by NAT_1:6;
defpred S₁[ Nat] means [(H1 \/ H2),phi] is m1 + 1,{[H1,phi]},{(R1 S)} -derivable ;
B2: [((H1 \/ H2) \/ (H1 \/ H2)),phi] is 1,{[(H1 \/ H2),phi]},{(R1 S)} -derivable ;
B0: S₁[ 0 ] ;
B1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then [(H1 \/ H2),phi] is (n + 1) + 1,{[H1,phi]},{(R1 S)} \/ {(R1 S)} -derivable by Lm28, B2;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(B0, B1);
hence for b₁ being set st b₁ = [((H1 \/ H2) null m1),phi] holds
b₁ is m1,{[H1,phi]},{(R1 S)} -derivable by B3; :: thesis: verum