set V = the infinite set ;
set E = the empty set ;
set f = the Function of the empty set , the infinite set ;
set G = createGraph ( the infinite set , the empty set , the Function of the empty set , the infinite set , the Function of the empty set , the infinite set );
take createGraph ( the infinite set , the empty set , the Function of the empty set , the infinite set , the Function of the empty set , the infinite set ) ; :: thesis: ( not createGraph ( the infinite set , the empty set , the Function of the empty set , the infinite set , the Function of the empty set , the infinite set ) is vertex-finite & createGraph ( the infinite set , the empty set , the Function of the empty set , the infinite set , the Function of the empty set , the infinite set ) is edge-finite )
thus ( not createGraph ( the infinite set , the empty set , the Function of the empty set , the infinite set , the Function of the empty set , the infinite set ) is vertex-finite & createGraph ( the infinite set , the empty set , the Function of the empty set , the infinite set , the Function of the empty set , the infinite set ) is edge-finite ) ; :: thesis: verum