let Y, Z be Subset of HP-WFF; :: thesis: ( ( for r being Element of HP-WFF holds
( r in Y iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) & ( for r being Element of HP-WFF holds
( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) implies Y = Z )
assume that
A2: for r being Element of HP-WFF holds
( r in Y iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) and
A3: for r being Element of HP-WFF holds
( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ; :: thesis: Y = Z
for a being object holds
( a in Y iff a in Z )

proof

let a be object ; :: thesis: ( a in Y iff a in Z )

hereby :: thesis: ( a in Z implies a in Y )

assume A4: a in Y ; :: thesis: a in Z
then reconsider t = a as Element of HP-WFF ;
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
t in T by A2, A4;
hence a in Z by A3; :: thesis: verum

end;

assume A5: a in Z ; :: thesis: a in Y
then reconsider t = a as Element of HP-WFF ;
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
t in T by A3, A5;
hence a in Y by A2; :: thesis: verum

end;

hence Y = Z by TARSKI:2; :: thesis: verum