set y = [H1,phi];
set SQ = {[H1,phi]};
set H = H1 \/ H2;
set Sq = [(H1 \/ H2),phi];
set Q = S -sequents ;
reconsider seqt = [(H1 \/ H2),phi] as Element of S -sequents by Def2;
reconsider Seqts = {[H1,phi]} as Element of bool (S -sequents) by Def3;
( H1 null H2 c= H1 \/ H2 & {[H1,phi]} \ {[H1,phi]} = {} & ([H1,phi] `1) \+\ H1 = {} & ([(H1 \/ H2),phi] `1) \+\ (H1 \/ H2) = {} & ([(H1 \/ H2),phi] `2) \+\ phi = {} & ([H1,phi] `2) \+\ phi = {} ) ;
then ( H1 c= H1 \/ H2 & [H1,phi] in {[H1,phi]} & [H1,phi] `1 = H1 & [(H1 \/ H2),phi] `1 = H1 \/ H2 & [(H1 \/ H2),phi] `2 = phi & [H1,phi] `2 = phi ) by FOMODEL0:29;
then seqt Rule1 Seqts ;
then [Seqts,seqt] in P#1 S by Def35;
then [(H1 \/ H2),phi] in (R#1 S) . {[H1,phi]} by Th3;
hence for b₁ being object st b₁ = [(H1 \/ H2),phi] holds
b₁ is 1,{[H1,phi]},{(R#1 S)} -derivable by Lm7; :: thesis: verum