let G be _Graph; :: thesis: for v, w being Vertex of G holds
( [v,w] in VertexAdjSymRel G iff v,w are_adjacent )
let v, w be Vertex of G; :: thesis: ( [v,w] in VertexAdjSymRel G iff v,w are_adjacent )
hereby :: thesis: ( v,w are_adjacent implies [v,w] in VertexAdjSymRel G )
assume [v,w] in VertexAdjSymRel G ; :: thesis: v,w are_adjacent
then consider e being object such that
A1: e Joins v,w,G by Th32;
thus v,w are_adjacent by A1, CHORD:def 3; :: thesis: verum
end;
assume v,w are_adjacent ; :: thesis: [v,w] in VertexAdjSymRel G
then consider e being object such that
A2: e Joins v,w,G by CHORD:def 3;
thus [v,w] in VertexAdjSymRel G by A2, Th32; :: thesis: verum