let V be non empty set ; :: thesis: for E being Relation of V holds
( V is trivial iff createGraph (V,E) is _trivial )
let E be Relation of V; :: thesis: ( V is trivial iff createGraph (V,E) is _trivial )
hereby :: thesis: ( createGraph (V,E) is _trivial implies V is trivial )
assume V is trivial ; :: thesis: createGraph (V,E) is _trivial
then the_Vertices_of (createGraph (V,E)) is trivial ;
then consider v being object such that
A1: the_Vertices_of (createGraph (V,E)) = {v} by ZFMISC_1:131;
card (the_Vertices_of (createGraph (V,E))) = 1 by A1, CARD_1:30;
hence createGraph (V,E) is _trivial ; :: thesis: verum
end;
assume createGraph (V,E) is _trivial ; :: thesis: V is trivial
then the_Vertices_of (createGraph (V,E)) is trivial ;
hence V is trivial ; :: thesis: verum