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