thus ( not C is void & not C is empty implies the Target of C . f is Vertex of C ) :: thesis: ( ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) & ( for b₁ being Vertex of C holds verum ) )

proof

assume ( not C is void & not C is empty ) ; :: thesis: the Target 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 Target of C . f is Vertex of C ;
hence the Target 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 ) & ( for b₁ being Vertex of C holds verum ) ) ; :: thesis: verum