set f = the union-distributive cap-distributive ManySortedSet of C;
take the union-distributive cap-distributive ManySortedSet of C ; :: thesis: the union-distributive cap-distributive ManySortedSet of C is U-linear
thus the union-distributive cap-distributive ManySortedSet of C is U-linear ; :: thesis: verum