theorem Th21: :: AOFA_L00:22

for n being natural non empty number
for X being set
for J being non empty Signature ex Q being non empty non void b₁ PC-correct QC-correct QCLangSignature over X st
( the carrier of Q misses the carrier of J & the carrier' of Q misses the carrier' of J )