let C be initialized ConstructorSignature; :: thesis: ( QuasiTerms C misses QuasiAdjs C & QuasiTerms C misses QuasiTypes C & QuasiTypes C misses QuasiAdjs C )
set X = MSVars C;
set Y = (MSVars C) \/ (the carrier of C --> {0 });
consider A being MSSubset of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) such that
A1: ( Free C,(MSVars C) = GenMSAlg A & A = (Reverse ((MSVars C) \/ (the carrier of C --> {0 }))) "" (MSVars C) ) by MSAFREE3:def 2;
the Sorts of (Free C,(MSVars C)) is MSSubset of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) by A1, MSUALG_2:def 10;
then A2: the Sorts of (Free C,(MSVars C)) c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) by PBOOLE:def 23;
A3: QuasiTerms C c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . (a_Term C) by A2, PBOOLE:def 5;
A4: the Sorts of (Free C,(MSVars C)) . (an_Adj C) c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . (an_Adj C) by A2, PBOOLE:def 5;
QuasiAdjs C c= the Sorts of (Free C,(MSVars C)) . (an_Adj C)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in QuasiAdjs C or x in the Sorts of (Free C,(MSVars C)) . (an_Adj C) )
assume x in QuasiAdjs C ; :: thesis: x in the Sorts of (Free C,(MSVars C)) . (an_Adj C)
then ex a being expression of C, an_Adj C st
( x = a & a is regular ) ;
hence x in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by ELEMENT; :: thesis: verum

end;

then A5: QuasiAdjs C c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . (an_Adj C) by A4, XBOOLE_1:1;
the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . (a_Term C) misses the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . (an_Adj C) by PROB_2:def 3;
hence QuasiTerms C misses QuasiAdjs C by A3, A5, XBOOLE_1:64; :: thesis: ( QuasiTerms C misses QuasiTypes C & QuasiTypes C misses QuasiAdjs C )

now

let x be set ; :: thesis: ( x in QuasiTerms C implies not x in QuasiTypes C )
assume ( x in QuasiTerms C & x in QuasiTypes C ) ; :: thesis: contradiction
then ( x is quasi-term of C & x is quasi-type of C ) by Th42, QUASITYPE;
hence contradiction ; :: thesis: verum

end;

hence QuasiTerms C misses QuasiTypes C by XBOOLE_0:3; :: thesis: QuasiTypes C misses QuasiAdjs C

now

let x be set ; :: thesis: ( x in QuasiAdjs C implies not x in QuasiTypes C )
assume ( x in QuasiAdjs C & x in QuasiTypes C ) ; :: thesis: contradiction
then ( x is quasi-adjective of C & x is quasi-type of C ) by Th52, QUASITYPE;
hence contradiction ; :: thesis: verum

end;

hence QuasiTypes C misses QuasiAdjs C by XBOOLE_0:3; :: thesis: verum