thus variables_in (a ast T) = (variables_in a) \/ (variables_in T) by Th102
.= {} \/ (variables_in T) by Th107
.= {} by Def50 ; :: according to ABCMIZ_1:def 50 :: thesis: verum