let Y be set ; :: thesis: ( Y = Theorems (X,R) iff for a being object holds
( a in Y iff X,R |- a ) )
thus ( Y = Theorems (X,R) implies for a being object holds
( a in Y iff X,R |- a ) ) :: thesis: ( ( for a being object holds
( a in Y iff X,R |- a ) ) implies Y = Theorems (X,R) )

proof

assume A1: Y = Theorems (X,R) ; :: thesis: for a being object holds
( a in Y iff X,R |- a )
let a be object ; :: thesis: ( a in Y iff X,R |- a )
thus ( a in Y implies X,R |- a ) :: thesis: ( X,R |- a implies a in Y )

proof

assume a in Y ; :: thesis: X,R |- a
then consider t being Element of X \/ (rng R) such that
A2: ( a = t & X,R |- t ) by A1;
thus X,R |- a by A2; :: thesis: verum

end;

assume A5: X,R |- a ; :: thesis: a in Y
then a in X \/ (rng R) by Lm54;
hence a in Y by A1, A5; :: thesis: verum

end;

assume A10: for a being object holds
( a in Y iff X,R |- a ) ; :: thesis: Y = Theorems (X,R)
thus Y c= Theorems (X,R) :: according to XBOOLE_0:def 10 :: thesis: Theorems (X,R) c= Y

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in Theorems (X,R) )
assume a in Y ; :: thesis: a in Theorems (X,R)
then ( a in X \/ (rng R) & X,R |- a ) by A10, Lm54;
hence a in Theorems (X,R) ; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Theorems (X,R) or a in Y )
assume a in Theorems (X,R) ; :: thesis: a in Y
then consider t being Element of X \/ (rng R) such that
A15: ( a = t & X,R |- t ) ;
thus a in Y by A10, A15; :: thesis: verum