defpred S₁[ set ] means v in $1;
consider X being set such that
A1: for z being set holds
( z in X iff ( z in the SEdges of G & S₁[z] ) ) from XFAMILY:sch 1();
A2: X c= the SEdges of G by A1;
the SEdges of G is finite by Th21;
then reconsider X = X as finite set by A2;
take card X ; :: thesis: ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & card X = card X )
take X ; :: thesis: ( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & card X = card X )
thus ( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & card X = card X ) by A1; :: thesis: verum