let i be Nat; :: thesis: for l being quasi-loci holds
( [(rng l),i] in Vars & l ^ <*[(rng l),i]*> is quasi-loci )
let l be quasi-loci; :: thesis: ( [(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; :: thesis: 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; :: thesis: verum