let x be variable; :: thesis: ( <*x*> is quasi-loci iff vars x = {} )
A1: <*x*> = (<*> Vars) ^ <*x*> by FINSEQ_1:34;
A2: rng {} = {} ;
( vars x c= {} implies vars x = {} ) ;
hence ( <*x*> is quasi-loci iff vars x = {} ) by A1, A2, Th29, Th31; :: thesis: verum