let G be Graph; :: thesis: ( G -SVSet {} = {} & G -TVSet {} = {} )
set X = {} ;

A1: now

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

end;

now

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

end;

hence ( G -SVSet {} = {} & G -TVSet {} = {} ) by A1; :: thesis: verum