set Q = S -sequents ;
reconsider Sq = [(Phi \/ {phi}),phi] as Element of S -sequents by DefSeqtLike;
reconsider E = {} as Subset of (S -sequents) by XBOOLE_1:2;
BB0: ( 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 Def0, BB0;
then [E,Sq] in P0 S by DefP0;
hence for b₁ being set st b₁ = [(Phi \/ {phi}),phi] holds
b₁ is 1, {} ,{(R0 S)} -derivable by Lm1b; :: thesis: verum