set V = the a -element set ;
set E = the b -element set ;
set v = the Element of the a -element set ;
set f = the b -element set --> the Element of the a -element set ;
reconsider f = the b -element set --> the Element of the a -element set as Function of the b -element set , the a -element set ;
take G = createGraph ( the a -element set , the b -element set ,f,f); :: thesis: ( G is a -vertex & G is b -edge )
( card the a -element set = a & card the b -element set = b ) by CARD_1:def 7;
hence ( G is a -vertex & G is b -edge ) ; :: thesis: verum