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