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