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 `2 = phi & Sq `1 = Phi \/ {phi} ) by MCART_1:7;
then Sq Rule0 E by Def18, A1;
then [E,Sq] in P#0 S by Def31;
hence for b₁ being set st b₁ = [(Phi \/ {phi}),phi] holds
b₁ is 1, {} ,{(R#0 S)} -derivable by Lm27; :: thesis: verum