consider f being union-distributive cap-distributive ManySortedSet of ;
take f ; :: thesis: f is U-linear
thus f is U-linear ; :: thesis: verum