let V be non empty set ; :: thesis: for E being Relation of V holds
( E is symmetric iff VertexAdjSymRel (createGraph (V,E)) = E )
let E be Relation of V; :: thesis: ( E is symmetric iff VertexAdjSymRel (createGraph (V,E)) = E )
set G = createGraph (V,E);
hereby :: thesis: ( VertexAdjSymRel (createGraph (V,E)) = E implies E is symmetric )
assume E is symmetric ; :: thesis: VertexAdjSymRel (createGraph (V,E)) = E
then A1: E = E ~ by RELAT_2:13;
thus VertexAdjSymRel (createGraph (V,E)) = E \/ ((VertexDomRel (createGraph (V,E))) ~)
.= E \/ (E ~)
.= E by A1 ; :: thesis: verum
end;
assume VertexAdjSymRel (createGraph (V,E)) = E ; :: thesis: E is symmetric
then E = E \/ ((VertexDomRel (createGraph (V,E))) ~)
.= E \/ (E ~) ;
then A2: E ~ c= E by XBOOLE_1:7;
then (E ~) ~ c= E ~ by SYSREL:11;
hence E is symmetric by A2, XBOOLE_0:def 10, RELAT_2:13; :: thesis: verum