set T = Theorems (X,R);
thus Theorems (X,R) is X -extending :: thesis: Theorems (X,R) is R -closed

proof

let a be object ; :: according to TARSKI:def 3,PROOFS_1:def 12 :: thesis: ( not a in X or a in Theorems (X,R) )
assume a in X ; :: thesis: a in Theorems (X,R)
then X,R |- a by Th46;
hence a in Theorems (X,R) by Def30r; :: thesis: verum

end;

let Y be set ; :: according to PROOFS_1:def 31 :: thesis: for a being object st [Y,a] in R & Y c= Theorems (X,R) holds
a in Theorems (X,R)
let a be object ; :: thesis: ( [Y,a] in R & Y c= Theorems (X,R) implies a in Theorems (X,R) )
assume that
A1: [Y,a] in R and
A2: Y c= Theorems (X,R) ; :: thesis: a in Theorems (X,R)
Y in dom R by A1, XTUPLE_0:def 12;
then reconsider S = Y as Formula-finset by Def1;
for b being object st b in S holds
X,R |- b

proof

let b be object ; :: thesis: ( b in S implies X,R |- b )
assume b in S ; :: thesis: X,R |- b
then b in Theorems (X,R) by A2;
then consider t being Element of X \/ (rng R) such that
A5: ( b = t & X,R |- t ) ;
thus X,R |- b by A5; :: thesis: verum

end;

then A6: X,R |- a by A1, Th49;
a in rng R by A1, XTUPLE_0:def 13;
then a in X \/ (rng R) by XBOOLE_0:def 3;
hence a in Theorems (X,R) by A6; :: thesis: verum