set A = the Axioms of P;
set R = the Rules of P;
set T = Theorems ( the Axioms of P, the Rules of P);
Theorems ( the Axioms of P, the Rules of P) c= the carrier of P

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Theorems ( the Axioms of P, the Rules of P) or a in the carrier of P )
assume a in Theorems ( the Axioms of P, the Rules of P) ; :: thesis: a in the carrier of P
then P |- a by Def30r;
hence a in the carrier of P by Th57; :: thesis: verum

end;

hence Theorems ( the Axioms of P, the Rules of P) is Subset of P ; :: thesis: verum