let G be Graph; :: thesis: for e, X being set st e in the carrier' of G & e in X holds
not G -VSet X is empty
let e, X be set ; :: thesis: ( e in the carrier' of G & e in X implies not G -VSet X is empty )
assume A1: ( e in the carrier' of G & e in X ) ; :: thesis: not G -VSet X is empty
then reconsider v = the Source of G . e as Vertex of G by FUNCT_2:7;
v in G -VSet X by A1;
hence not G -VSet X is empty ; :: thesis: verum