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});
ex A being MSSubset of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) st
( Free (C,(MSVars C)) = GenMSAlg A & A = (Reverse ((MSVars C) (\/) ( the carrier of C --> {0}))) "" (MSVars C) ) by MSAFREE3:def 1;
then the Sorts of (Free (C,(MSVars C))) is MSSubset of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) by MSUALG_2:def 9;
then A1: the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) by PBOOLE:def 18;
then A2: QuasiTerms C c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . (a_Term C) ;
A3: 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 A1;
QuasiAdjs C c= the Sorts of (Free (C,(MSVars C))) . (an_Adj C)
proof
let x be object ; :: 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 Def28; :: thesis: verum
end;
then A4: QuasiAdjs C c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . (an_Adj C) by A3;
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 2;
hence QuasiTerms C misses QuasiAdjs C by A2, A4, XBOOLE_1:64; :: thesis: ( QuasiTerms C misses QuasiTypes C & QuasiTypes C misses QuasiAdjs C )
now :: thesis: for x being object st x in QuasiTerms C holds
not x in QuasiTypes C
let x be object ; :: thesis: ( x in QuasiTerms C implies not x in QuasiTypes C )
assume that
A5: x in QuasiTerms C and
A6: x in QuasiTypes C ; :: thesis: contradiction
x is quasi-type of C by A6, Def43;
hence contradiction by A5; :: thesis: verum
end;
hence QuasiTerms C misses QuasiTypes C by XBOOLE_0:3; :: thesis: QuasiTypes C misses QuasiAdjs C
now :: thesis: for x being object st x in QuasiAdjs C holds
not x in QuasiTypes C
let x be object ; :: thesis: ( x in QuasiAdjs C implies not x in QuasiTypes C )
assume that
A7: x in QuasiAdjs C and
A8: x in QuasiTypes C ; :: thesis: contradiction
x is quasi-type of C by A8, Def43;
hence contradiction by A7; :: thesis: verum
end;
hence QuasiTypes C misses QuasiAdjs C by XBOOLE_0:3; :: thesis: verum