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 )

( 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

hence
Y = Z
by TARSKI:2; :: thesis: verum
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 )

end;thus ( a in Y implies a in Z ) :: thesis: ( a in Z implies a in Y )

proof

thus
( a in Z implies a in Y )
:: thesis: verum
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;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

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;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