X c= X ;
then reconsider Z = X as Subset of X ;
take Z ; :: thesis: Z is F -binopclosed
thus Z is F -binopclosed by Th1; :: thesis: verum