assume Vars meets Constructors ; :: thesis: contradiction
then consider x being object such that
A1: ( x in Vars & x in Constructors ) by XBOOLE_0:3;
reconsider x = x as Element of Vars by A1;
consider A being Subset of Vars, j being Element of NAT such that
A2: ( x = [(varcl A),j] & A is finite ) by A1, ABCMIZ_1:18;
( x in Modes \/ Attrs or x in Funcs ) by A1, XBOOLE_0:def 3;
then ( x in Modes or x in Attrs or x in Funcs ) by XBOOLE_0:def 3;
then ( x `2 in [:QuasiLoci,NAT:] & x `2 = j ) by A2, MCART_1:10;
then ex a, b being object st
( a in QuasiLoci & b in NAT & [a,b] = j ) by ZFMISC_1:def 2;
hence contradiction ; :: thesis: verum