let G be _Graph; :: thesis: for v, w being Vertex of G st H₇(G,v) meets H₇(G,w) holds
v = w
let v, w be Vertex of G; :: thesis: ( H₇(G,v) meets H₇(G,w) implies v = w )
assume H₇(G,v) meets H₇(G,w) ; :: thesis: v = w
then consider z being object such that
A1: ( z in H₇(G,v) & z in H₇(G,w) ) by XBOOLE_0:3;
consider w0, x0, y0 being object such that
A2: ( w0 in {v} & x0 in v .edgesIn() & y0 in {1} & z = [w0,x0,y0] ) by A1, MCART_1:68;
consider w1, x1, y1 being object such that
A3: ( w1 in {w} & x1 in w .edgesIn() & y1 in {1} & z = [w1,x1,y1] ) by A1, MCART_1:68;
( w0 = v & w1 = w ) by A2, A3, TARSKI:def 1;
hence v = w by A2, A3, XTUPLE_0:3; :: thesis: verum