consider X being non empty finite set , P being a_partition of X;
take M = ProdMatroid P; :: thesis: ( M is finite & M is strict )
thus ( M is finite & M is strict ) ; :: thesis: verum