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