let V be non empty set ; :: thesis: for E being Relation of V holds
( E is antisymmetric iff createGraph (V,E) is non-multi )
let E be Relation of V; :: thesis: ( E is antisymmetric iff createGraph (V,E) is non-multi )
set G0 = createGraph (V,E);

hereby :: thesis: ( createGraph (V,E) is non-multi implies E is antisymmetric )

assume E is antisymmetric ; :: thesis: createGraph (V,E) is non-multi
then A1: E is_antisymmetric_in field E by RELAT_2:def 12;
assume not createGraph (V,E) is non-multi ; :: thesis: contradiction
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 ( ( e1 DJoins v,w, createGraph (V,E) & e2 DJoins v,w, createGraph (V,E) ) or ( e1 DJoins v,w, createGraph (V,E) & e2 DJoins w,v, createGraph (V,E) ) or ( e1 DJoins w,v, createGraph (V,E) & e2 DJoins v,w, createGraph (V,E) ) or ( e1 DJoins w,v, createGraph (V,E) & e2 DJoins w,v, createGraph (V,E) ) ) by A2, GLIB_000:16;

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

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

end;

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

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: verum

end;

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

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: verum

end;

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

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

end;

end;

end;

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