theorem Th31: :: ABCMIZ_1:31

for l being quasi-loci
for x being variable holds
( l ^ <*x*> is quasi-loci iff ( not x in rng l & vars x c= rng l ) )