thus ( not C is void & not C is empty implies the Source of C . f is Vertex of C ) :: thesis: ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C )

proof

assume ( not C is void & not C is empty ) ; :: thesis: the Source of C . f is Vertex of C
then reconsider C = C as non empty non void MultiGraphStruct ;
reconsider f = f as Edge of C ;
the Source of C . f is Vertex of C ;
hence the Source of C . f is Vertex of C ; :: thesis: verum

end;

thus ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) ; :: thesis: verum