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 consider v being Element of the carrier of G such that
A3: ( v = x & ex e being Element of the carrier' of G st
( e in {} & v = the Source of G . e ) ) ;
consider e being Element of the carrier' of G such that
A4: ( e in {} & v = the Source of G . e ) by A3;
thus contradiction by A4; :: thesis: verum

end;

now

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

end;

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