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 that
A1: e in the carrier' of G and
A2: e in X ; :: thesis: not G -VSet X is empty
reconsider v = the Source of G . e as Vertex of G by A1, FUNCT_2:5;
v in G -VSet X by A1, A2;
hence not G -VSet X is empty ; :: thesis: verum