set V = {1};
set E = {1};
reconsider j = 1 as Element of {1} by TARSKI:def 1;
reconsider S = {1} --> j, T = {1} --> j as Function of {1},{1} ;
reconsider G = MultiGraphStruct(# {1},{1},S,T #) as Graph ;
reconsider v = 1 as Element of the carrier of G ;
take G ; :: thesis: not G is well-founded
A1: S . 1 = 1 by FUNCOP_1:7;
A2: G is with_directed_cycle

proof

reconsider dc = <*1*> as directed Chain of G by Th4;
take dc ; :: according to MSSCYC_1:def 3 :: thesis: ( not dc is empty & dc is cyclic )
thus not dc is empty ; :: thesis: dc is cyclic
A3: ( <*v,v*> . 2 = v & len <*v,v*> = 2 ) by FINSEQ_1:44;
( <*v,v*> is_vertex_seq_of dc & <*v,v*> . 1 = v ) by A1, Th3;
hence dc is cyclic by A3; :: thesis: verum

end;

assume G is well-founded ; :: thesis: contradiction
then reconsider G = G as well-founded Graph ;
G is directed_cycle-less ;
hence contradiction by A2; :: thesis: verum