theorem :: ABCMIZ_1:36
for x, y, z being variable holds
( <*x,y,z*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} & x <> z & y <> z & vars z c= {x,y} ) )