let Y, Z be Subset of (CQC-WFF Al); :: thesis: ( ( for t being Element of CQC-WFF Al holds
( t in Y iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T ) ) & ( for t being Element of CQC-WFF Al holds
( t in Z iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T ) ) implies Y = Z )

assume that
A2: for t being Element of CQC-WFF Al holds
( t in Y iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T ) and
A3: for t being Element of CQC-WFF Al holds
( t in Z iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t 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 )
thus ( a in Y implies a in Z ) :: thesis: ( a in Z implies a in Y )
proof
assume A4: a in Y ; :: thesis: a in Z
then reconsider t = a as Element of CQC-WFF Al ;
for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T by A2, A4;
hence a in Z by A3; :: thesis: verum
end;
thus ( a in Z implies a in Y ) :: thesis: verum
proof
assume A5: a in Z ; :: thesis: a in Y
then reconsider t = a as Element of CQC-WFF Al ;
for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T by A3, A5;
hence a in Y by A2; :: thesis: verum
end;
end;
hence Y = Z by TARSKI:2; :: thesis: verum