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 )
for x being Nat holds
( GSq . x is connected & GSq . x is acyclic & GSq . x is Tree-like )

proof

let x be Nat; :: thesis: ( GSq . x is connected & GSq . x is acyclic & GSq . x is Tree-like )
x in NAT by ORDINAL1:def 12;
then GSq . x = the Tree-like _Graph by FUNCOP_1:7;
hence ( GSq . x is connected & GSq . x is acyclic & GSq . x is Tree-like ) ; :: thesis: verum

end;

hence ( GSq is connected & GSq is acyclic & GSq is Tree-like & not GSq is empty ) ; :: thesis: verum