set B = the carrier of G;
take card the carrier of G ; :: thesis: ex B being finite set st
( B = the carrier of G & card the carrier of G = card B )
take the carrier of G ; :: thesis: ( the carrier of G = the carrier of G & card the carrier of G = card the carrier of G )
thus ( the carrier of G = the carrier of G & card the carrier of G = card the carrier of G ) ; :: thesis: verum