let S be non void Signature; :: thesis: for X being V5() ManySortedSet of
for t being Term of S,X holds variables_in t = X variables_in t
let X be V5() ManySortedSet of ; :: thesis: for t being Term of S,X holds variables_in t = X variables_in t
let t be Term of S,X; :: thesis: variables_in t = X variables_in t
S variables_in t c= X by Th15;
hence variables_in t = X variables_in t by PBOOLE:25; :: thesis: verum