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