let C be initialized ConstructorSignature; :: thesis: for q being pure expression of C, a_Type C holds variables_in (({} (QuasiAdjs C)) ast q) = variables_in q
let q be pure expression of C, a_Type C; :: thesis: variables_in (({} (QuasiAdjs C)) ast q) = variables_in q
set A = {} (QuasiAdjs C);
set AA = { (variables_in a) where a is quasi-adjective of C : a in {} (QuasiAdjs C) } ;
{ (variables_in a) where a is quasi-adjective of C : a in {} (QuasiAdjs C) } c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (variables_in a) where a is quasi-adjective of C : a in {} (QuasiAdjs C) } or x in {} )
assume x in { (variables_in a) where a is quasi-adjective of C : a in {} (QuasiAdjs C) } ; :: thesis: x in {}
then ex a being quasi-adjective of C st
( x = variables_in a & a in {} (QuasiAdjs C) ) ;
hence x in {} ; :: thesis: verum

end;

then A1: { (variables_in a) where a is quasi-adjective of C : a in {} (QuasiAdjs C) } = {} ;
variables_in (({} (QuasiAdjs C)) ast q) = (union { (variables_in a) where a is quasi-adjective of C : a in {} (QuasiAdjs C) } ) \/ (variables_in q) by Th104;
hence variables_in (({} (QuasiAdjs C)) ast q) = variables_in q by A1, ZFMISC_1:2; :: thesis: verum