set Q = S -sequents ;
reconsider Sq = [(Phi \/ {phi}),phi] as Element of S -sequents by Def2;
reconsider E = {} as Subset of (S -sequents) by XBOOLE_1:2;
A1: ( phi in {phi} & {phi} c= Phi \/ {phi} ) by TARSKI:def 1, XBOOLE_1:7;
Sq Rule0 E by A1;
then [E,Sq] in P#0 S by Def34;
hence for b₁ being object st b₁ = [(Phi \/ {phi}),phi] holds
b₁ is 1, {} ,{(R#0 S)} -derivable by Lm28; :: thesis: verum