let x, y, z be variable; :: thesis: ( <*x,y,z*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} & x <> z & y <> z & vars z c= {x,y} ) )
A1: rng <*x,y*> = {x,y} by FINSEQ_2:127;
A2: ( <*x,y*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} ) ) by Th35;
( z in {x,y} iff ( z = x or z = y ) ) by TARSKI:def 2;
hence ( <*x,y,z*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} & x <> z & y <> z & vars z c= {x,y} ) ) by A1, A2, Th31, Th32; :: thesis: verum