let G be _Graph; :: thesis: for v0, v1 being Vertex of G holds H₆(G,v0) misses H₇(G,v1)
let v0, v1 be Vertex of G; :: thesis: H₆(G,v0) misses H₇(G,v1)
assume H₆(G,v0) meets H₇(G,v1) ; :: thesis: contradiction
then consider z being object such that
A1: ( z in H₆(G,v0) & z in H₇(G,v1) ) by XBOOLE_0:3;
H₆(G,v0) = [:[:{v0},(v0 .edgesOut()):],{0}:] by ZFMISC_1:def 3;
then consider z0, y0 being object such that
A2: ( z0 in [:{v0},(v0 .edgesOut()):] & y0 in {0} & z = [z0,y0] ) by A1, ZFMISC_1:def 2;
H₇(G,v1) = [:[:{v1},(v1 .edgesIn()):],{1}:] by ZFMISC_1:def 3;
then consider z1, y1 being object such that
A3: ( z1 in [:{v1},(v1 .edgesIn()):] & y1 in {1} & z = [z1,y1] ) by A1, ZFMISC_1:def 2;
( y0 = 0 & y1 = 1 ) by A2, A3, TARSKI:def 1;
hence contradiction by A2, A3, XTUPLE_0:1; :: thesis: verum