take F = pr1 (X,X); :: thesis: F is A -subsetpreserving
A is F -binopclosed by Th3;
hence F is A -subsetpreserving ; :: thesis: verum