let i be Nat; for l being quasi-loci holds
( [(rng l),i] in Vars & l ^ <*[(rng l),i]*> is quasi-loci )
let l be quasi-loci; ( [(rng l),i] in Vars & l ^ <*[(rng l),i]*> is quasi-loci )
varcl (rng l) = rng l
by ABCMIZ_1:33;
hence
[(rng l),i] in Vars
by ABCMIZ_1:17; l ^ <*[(rng l),i]*> is quasi-loci
then reconsider x = [(rng l),i] as variable ;
( rng l in {(rng l),i} & {(rng l),i} in x )
by TARSKI:def 2;
then
( vars x = rng l & x nin rng l )
by XREGULAR:7;
hence
l ^ <*[(rng l),i]*> is quasi-loci
by ABCMIZ_1:31; verum