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
A6: 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
reconsider t = a as Element of CQC-WFF by A7;
A8: for T being Subset of CQC-WFF st T is being_a_theory & X c= T holds
t in T by A4, A7;
thus a in Z by A5, A8; :: thesis: verum

end;

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

proof

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

end;

end;

thus Y = Z by A6, TARSKI:2; :: thesis: verum