reconsider GSq = NAT --> the Tree-like _Graph as GraphSeq ;
take GSq ; :: thesis: ( GSq is connected & GSq is acyclic & GSq is Tree-like & not GSq is empty )
thus ( GSq is connected & GSq is acyclic & GSq is Tree-like & not GSq is empty ) ; :: thesis: verum