let G be Graph; :: thesis: G -VSet {} = {}
assume not G -VSet {} = {} ; :: thesis: contradiction
then consider x being object such that
A1: x in G -VSet {} by XBOOLE_0:def 1;
ex v being Vertex of G st
( 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;
hence contradiction ; :: thesis: verum