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 DefSeqtLike;
reconsider Seqts = {} null S as Element of bool (S -sequents) by DefSeqtLike2;
( ([(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, ZFMISC_1:60;
then seqt Rule0 Seqts by Def0;
then [Seqts,seqt] in P0 S by DefP0;
then [(H \/ {phi}),phi] in (R0 S) . ({} null S) by Th3;
hence for b₁ being set st b₁ = [(H \/ {phi}),phi] holds
b₁ is 1, {} ,{(R0 S)} -derivable by Lm22; :: thesis: verum