set f = id (Union the Sorts of (Free S,X));
A1: dom (id (Union the Sorts of (Free S,X))) = Union the Sorts of (Free S,X) by RELAT_1:71;
rng (id (Union the Sorts of (Free S,X))) = Union the Sorts of (Free S,X) by RELAT_1:71;
then reconsider f = id (Union the Sorts of (Free S,X)) as UnOp of (Union the Sorts of (Free S,X)) by A1, FUNCT_2:4;
take f ; :: thesis: for s being SortSymbol of S holds f .: (the Sorts of (Free S,X) . s) c= the Sorts of (Free S,X) . s
thus for s being SortSymbol of S holds f .: (the Sorts of (Free S,X) . s) c= the Sorts of (Free S,X) . s by Th4; :: thesis: verum