let G be SimpleGraph; :: thesis: ( Vertices G is finite implies G is finite )
assume A1: Vertices G is finite ; :: thesis: G is finite
G c= bool (Vertices G) by ZFMISC_1:82;
hence G is finite by A1; :: thesis: verum