let x, y be variable; :: thesis: ( <*x,y*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} ) )
A2: rng <*x*> = {x} by FINSEQ_1:55;
A3: ( <*x*> is quasi-loci iff vars x = {} ) by Th33;
( 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 A2, A3, Th6, Th7; :: thesis: verum