thus variables_in (a ast T) = (variables_in a) \/ (variables_in T) by Th72
.= {} \/ (variables_in T) by ThG
.= {} by GROUND2 ; :: according to ABCMIZ_1:def 50 :: thesis: verum