let V be non empty set ; :: thesis:
let E be Relation of V; :: thesis:
set G0 = createGraph (V,E);

hereby :: thesis:

assume E is antisymmetric ; :: thesis:
then A1: E is_antisymmetric_in field E by RELAT_2:def 12;
assume not createGraph (V,E) is non-multi ; :: thesis:
then consider e1, e2, v, w being object such that
A2: ( e1 Joins v,w, createGraph (V,E) & e2 Joins v,w, createGraph (V,E) & e1 <> e2 ) by GLIB_000:def 20;
( e1 in the_Edges_of (createGraph (V,E)) & e2 in the_Edges_of (createGraph (V,E)) ) by A2, GLIB_000:def 13;
then A3: ( e1 in E & e2 in E ) ;

per cases by A2, GLIB_000:16;

suppose ( e1 DJoins v,w, createGraph (V,E) & e2 DJoins v,w, createGraph (V,E) ) ; :: thesis:

then ( e1 = [v,w] & e2 = [v,w] ) by Th64;
hence contradiction by A2; :: thesis:

end;

suppose ( e1 DJoins v,w, createGraph (V,E) & e2 DJoins w,v, createGraph (V,E) ) ; :: thesis:

then A4: ( e1 = [v,w] & e2 = [w,v] ) by Th64;
then ( v in field E & w in field E ) by A3, RELAT_1:15;
then v = w by A1, A3, A4, RELAT_2:def 4;
hence contradiction by A2, A4; :: thesis:

end;

suppose ( e1 DJoins w,v, createGraph (V,E) & e2 DJoins v,w, createGraph (V,E) ) ; :: thesis:

then A5: ( e1 = [w,v] & e2 = [v,w] ) by Th64;
then ( v in field E & w in field E ) by A3, RELAT_1:15;
then v = w by A1, A3, A5, RELAT_2:def 4;
hence contradiction by A2, A5; :: thesis:

end;

suppose ( e1 DJoins w,v, createGraph (V,E) & e2 DJoins w,v, createGraph (V,E) ) ; :: thesis:

then ( e1 = [w,v] & e2 = [w,v] ) by Th64;
hence contradiction by A2; :: thesis:

end;

end;

end;

assume createGraph (V,E) is non-multi ; :: thesis:
then VertexDomRel (createGraph (V,E)) is antisymmetric ;
hence E is antisymmetric ; :: thesis: