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