let G1 be _Graph; :: thesis: for G2 being GraphComplement of G1 holds
( G1 is _trivial iff G2 is _trivial )
let G2 be GraphComplement of G1; :: thesis: ( G1 is _trivial iff G2 is _trivial )

hereby :: thesis: ( G2 is _trivial implies G1 is _trivial )

assume G1 is _trivial ; :: thesis: G2 is _trivial
then 1 = G1 .order() by GLIB_000:26
.= G2 .order() by Th111 ;
hence G2 is _trivial by GLIB_000:26; :: thesis: verum

end;

hereby :: thesis: verum

assume G2 is _trivial ; :: thesis: G1 is _trivial
then 1 = G2 .order() by GLIB_000:26
.= G1 .order() by Th111 ;
hence G1 is _trivial by GLIB_000:26; :: thesis: verum

end;