assume A2: G -SVSet {} <> {} ; :: thesis: contradiction
set x = the Element of G -SVSet {};
the Element of G -SVSet {} in G -SVSet {} by A2;
then ex v being Element of G st
( v = the Element of G -SVSet {} & ex e being Element of the carrier' of G st
( e in {} & v = the Source of G . e ) ) ;
hence contradiction ; :: thesis: verum

assume A3: G -TVSet {} <> {} ; :: thesis: contradiction
set x = the Element of G -TVSet {};
the Element of G -TVSet {} in G -TVSet {} by A3;
then ex v being Element of G st
( v = the Element of G -TVSet {} & ex e being Element of the carrier' of G st
( e in {} & v = the Target of G . e ) ) ;
hence contradiction ; :: thesis: verum