thus X (/\) (S variables_in t) c= X by PBOOLE:15; :: according to PBOOLE:def 18 :: thesis: verum