set V = {1};

set E = {} ;

reconsider S = {} as Function of {},{1} by RELSET_1:12;

set G = createGraph ({1},{},S,S);

take createGraph ({1},{},S,S) ; :: thesis: ( createGraph ({1},{},S,S) is trivial & createGraph ({1},{},S,S) is finite & createGraph ({1},{},S,S) is Tree-like )

thus ( createGraph ({1},{},S,S) is trivial & createGraph ({1},{},S,S) is finite & createGraph ({1},{},S,S) is Tree-like ) ; :: thesis: verum

set E = {} ;

reconsider S = {} as Function of {},{1} by RELSET_1:12;

set G = createGraph ({1},{},S,S);

take createGraph ({1},{},S,S) ; :: thesis: ( createGraph ({1},{},S,S) is trivial & createGraph ({1},{},S,S) is finite & createGraph ({1},{},S,S) is Tree-like )

thus ( createGraph ({1},{},S,S) is trivial & createGraph ({1},{},S,S) is finite & createGraph ({1},{},S,S) is Tree-like ) ; :: thesis: verum