let GSq be GraphSeq; :: thesis: ( GSq is trivial implies GSq is connected )
assume A1: GSq is trivial ; :: thesis: GSq is connected
let n be Nat; :: according to GLIB_002:def 12 :: thesis: GSq . n is connected
reconsider G = GSq . n as trivial _Graph by A1;
G is connected ;
hence GSq . n is connected ; :: thesis: verum