let V be non empty set ; :: thesis: for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for v being Vertex of G holds
( v is isolated iff not v in field E )
let E be symmetric Relation of V; :: thesis: for G being GraphFromSymRel of V,E
for v being Vertex of G holds
( v is isolated iff not v in field E )
let G be GraphFromSymRel of V,E; :: thesis: for v being Vertex of G holds
( v is isolated iff not v in field E )
let v be Vertex of G; :: thesis: ( v is isolated iff not v in field E )
set G0 = createGraph (V,E);
consider E0 being RepEdgeSelection of createGraph (V,E) such that
A1: G is inducedSubgraph of createGraph (V,E), the_Vertices_of (createGraph (V,E)),E0 by GLIB_009:def 7;
A2: the_Edges_of (createGraph (V,E)) = (createGraph (V,E)) .edgesBetween (the_Vertices_of (createGraph (V,E))) by GLIB_000:34;
the_Vertices_of (createGraph (V,E)) c= the_Vertices_of (createGraph (V,E)) ;
then reconsider v0 = v as Vertex of (createGraph (V,E)) by A1, A2, GLIB_000:def 37;
( v is isolated iff v0 is isolated ) by GLIB_009:111;
hence ( v is isolated iff not v in field E ) by Th83; :: thesis: verum