defpred S₁[ object ] means ex w being Vertex of G st
( $1 = w & w is endvertex );
consider M being Subset of (the_Vertices_of G) such that
A1: for v being set holds
( v in M iff ( v in the_Vertices_of G & S₁[v] ) ) from SUBSET_1:sch 1();
take M ; :: thesis: for v being object holds
( v in M iff ex w being Vertex of G st
( v = w & w is endvertex ) )
thus for v being object holds
( v in M iff ex w being Vertex of G st
( v = w & w is endvertex ) ) by A1; :: thesis: verum