let G be _Graph; :: thesis: H₈(G) is mutually-disjoint

now :: thesis: for x, y being set st x in H₈(G) & y in H₈(G) & x <> y holds
not x meets y

let x, y be set ; :: thesis: ( x in H₈(G) & y in H₈(G) & x <> y implies not x meets y )
assume A1: ( x in H₈(G) & y in H₈(G) & x <> y ) ; :: thesis: not x meets y
then consider v being Vertex of G such that
A2: ( x = H₆(G,v) \/ H₇(G,v) & not v is isolated ) ;
consider w being Vertex of G such that
A3: ( y = H₆(G,w) \/ H₇(G,w) & not w is isolated ) by A1;
assume x meets y ; :: thesis: contradiction
then consider z being object such that
A4: ( z in x & z in y ) by XBOOLE_0:3;

per cases ( ( z in H₆(G,v) & z in H₆(G,w) ) or ( z in H₆(G,v) & z in H₇(G,w) ) or ( z in H₇(G,v) & z in H₆(G,w) ) or ( z in H₇(G,v) & z in H₇(G,w) ) ) by A2, A3, A4, XBOOLE_0:def 3;

suppose ( z in H₆(G,v) & z in H₆(G,w) ) ; :: thesis: contradiction

then v = w by Lm12, XBOOLE_0:3;
hence contradiction by A1, A2, A3; :: thesis: verum

end;

suppose ( z in H₆(G,v) & z in H₇(G,w) ) ; :: thesis: contradiction

hence contradiction by Lm10, XBOOLE_0:3; :: thesis: verum

end;

suppose ( z in H₇(G,v) & z in H₆(G,w) ) ; :: thesis: contradiction

hence contradiction by Lm10, XBOOLE_0:3; :: thesis: verum

end;

suppose ( z in H₇(G,v) & z in H₇(G,w) ) ; :: thesis: contradiction

then v = w by Lm13, XBOOLE_0:3;
hence contradiction by A1, A2, A3; :: thesis: verum

end;

end;

end;

hence H₈(G) is mutually-disjoint by TAXONOM2:def 5; :: thesis: verum