let Y, Z be Subset of CQC-WFF ; :: thesis: ( ( for t being Element of CQC-WFF holds
( t in Y iff for T being Subset of CQC-WFF st T is being_a_theory & X c= T holds
t in T ) ) & ( for t being Element of CQC-WFF holds
( t in Z iff for T being Subset of CQC-WFF st T is being_a_theory & X c= T holds
t in T ) ) implies Y = Z )
assume that
A4: for t being Element of CQC-WFF holds
( t in Y iff for T being Subset of CQC-WFF st T is being_a_theory & X c= T holds
t in T ) and
A5: for t being Element of CQC-WFF holds
( t in Z iff for T being Subset of CQC-WFF st T is being_a_theory & X c= T holds
t in T ) ; :: thesis: Y = Z
for a being set holds
( a in Y iff a in Z )

proof

let a be set ; :: thesis: ( a in Y iff a in Z )
thus ( a in Y implies a in Z ) :: thesis: ( a in Z implies a in Y )

proof

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

end;

thus ( a in Z implies a in Y ) :: thesis: verum

proof

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

end;

end;

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