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

now

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

end;

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