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

A1: now :: thesis: not G -SVSet {} <> {}

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

end;

now :: thesis: not G -TVSet {} <> {}

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

end;

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