set V = {1};
set E = {} ;
set S = the Function of {},{1};
reconsider G = MultiGraphStruct(# {1},{}, the Function of {},{1}, the Function of {},{1} #) as Graph ;
take G ; :: thesis: G is void
thus the carrier' of G is empty ; :: according to STRUCT_0:def 13 :: thesis: verum