set Y = { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ;
set X = { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;
reconsider Z = still_not-bound_in p as finite set by CQC_SIM1:19;
for a being object holds
( a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } iff a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } )

let a be object ; :: thesis:
thus ( a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } implies a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ) :: thesis:

assume a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ; :: thesis:
then consider y being bound_QC-variable of A such that
A1: ( a = y & y in still_not-bound_in p ) and
A2: ( y is Element of dom Sub & y <> x & y <> Sub . y ) ;
y in { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } by A2;
hence a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } by A1, XBOOLE_0:def 4; :: thesis:

end;

thus ( a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } implies a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ) :: thesis:

assume A3: a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ; :: thesis:
then a in { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } by XBOOLE_0:def 4;
then A4: ex y being bound_QC-variable of A st
( a = y & y is Element of dom Sub & y <> x & y <> Sub . y ) ;
a in Z by A3, XBOOLE_0:def 4;
hence a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A4; :: thesis:

end;

then reconsider X = { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } as finite set by TARSKI:2;
Sub | X is finite ;
hence Sub | { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } is finite CQC_Substitution of A ; :: thesis: