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 b1 being object st b1 = [(H1 \/ H2),phi] holds
b1 is 1,{[H1,phi]},{(R#1 S)} -derivable
by Lm7; verum