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 XBOOLE_0:sch 1();
A2: X c= the SEdges of G

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in the SEdges of G )
assume z in X ; :: thesis: z in the SEdges of G
hence z in the SEdges of G by A1; :: thesis: verum

end;

the SEdges of G is finite by Th27;
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