let S be non void Signature; :: thesis: for X being V5() ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t = X variables_in t
let X be V5() ManySortedSet of the carrier of S; :: 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