let C be standardized ConstructorSignature; :: thesis: Vars misses the carrier' of C
assume Vars meets the carrier' of C ; :: thesis: contradiction
then consider x being object such that
A1: ( x in Vars & x in the carrier' of C ) by XBOOLE_0:3;
reconsider x = x as Element of Vars by A1;
reconsider c = x as OperSymbol of C by A1;
( x = * or x = non_op or c is constructor ) ;
then ( x = * or x = non_op or ( x in Constructors & Vars misses Constructors ) ) by Th8, Def1;
hence contradiction by XBOOLE_0:3; :: thesis: verum