take (0). G ; :: thesis: ( (0). G is strict & (0). G is finite )
thus ( (0). G is strict & (0). G is finite ) ; :: thesis: verum