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