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