let G be Graph; :: thesis: G -VSet {} = {}
assume not G -VSet {} = {} ; :: thesis: contradiction
then consider x being set such that
A1: x in G -VSet {} by XBOOLE_0:def 1;
consider v being Vertex of G such that
A2: ( x = v & ex e being Element of the carrier' of G st
( e in {} & ( v = the Source of G . e or v = the Target of G . e ) ) ) by A1;
consider e being Element of the carrier' of G such that
A3: ( e in {} & ( v = the Source of G . e or v = the Target of G . e ) ) by A2;
thus contradiction by A3; :: thesis: verum