let GSq be GraphSeq; :: thesis: ( GSq is acyclic implies GSq is simple )
assume A1: GSq is acyclic ; :: thesis: GSq is simple

now :: thesis: for n being Nat holds GSq . n is simple

let n be Nat; :: thesis: GSq . n is simple
reconsider G = GSq . n as acyclic _Graph by A1;
G is simple ;
hence GSq . n is simple ; :: thesis: verum

end;

hence GSq is simple by GLIB_000:def 63; :: thesis: verum