let x, y be variable; :: thesis: ( <*x,y*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} ) )
A1: rng <*x*> = {x} by FINSEQ_1:38;
A2: ( <*x*> is quasi-loci iff vars x = {} ) by Th34;
( y in {x} iff y = x ) by TARSKI:def 1;
hence ( <*x,y*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} ) ) by A1, A2, Th31, Th32; :: thesis: verum