let G be _Graph; :: thesis: for C being Component of G holds Endvertices C c= Endvertices G
let C be Component of G; :: thesis: Endvertices C c= Endvertices G

now :: thesis: for x being object st x in Endvertices C holds
x in Endvertices G

let x be object ; :: thesis: ( x in Endvertices C implies x in Endvertices G )
assume x in Endvertices C ; :: thesis: x in Endvertices G
then consider v being Vertex of C such that
A1: ( x = v & v is endvertex ) by GLIB_006:def 8;
the_Vertices_of C c= the_Vertices_of G ;
then reconsider w = v as Vertex of G by TARSKI:def 3;
1 = v .degree() by A1, GLIB_000:174
.= w .degree() by GLIBPRE0:44 ;
hence x in Endvertices G by A1, GLIB_000:174, GLIB_006:56; :: thesis: verum

end;

hence Endvertices C c= Endvertices G by TARSKI:def 3; :: thesis: verum