let X, Y be set ; :: thesis: ( ( for a being object holds

( a in X iff a is FinSequence of CQC-WFF Al ) ) & ( for a being object holds

( a in Y iff a is FinSequence of CQC-WFF Al ) ) implies X = Y )

assume that

A2: for a being object holds

( a in X iff a is FinSequence of CQC-WFF Al ) and

A3: for a being object holds

( a in Y iff a is FinSequence of CQC-WFF Al ) ; :: thesis: X = Y

( a in X iff a is FinSequence of CQC-WFF Al ) ) & ( for a being object holds

( a in Y iff a is FinSequence of CQC-WFF Al ) ) implies X = Y )

assume that

A2: for a being object holds

( a in X iff a is FinSequence of CQC-WFF Al ) and

A3: for a being object holds

( a in Y iff a is FinSequence of CQC-WFF Al ) ; :: thesis: X = Y

now :: thesis: for a being object holds

( a in X iff a in Y )

hence
X = Y
by TARSKI:2; :: thesis: verum( a in X iff a in Y )

let a be object ; :: thesis: ( a in X iff a in Y )

( a in X iff a is FinSequence of CQC-WFF Al ) by A2;

hence ( a in X iff a in Y ) by A3; :: thesis: verum

end;( a in X iff a is FinSequence of CQC-WFF Al ) by A2;

hence ( a in X iff a in Y ) by A3; :: thesis: verum