let S be non empty Graph-membered vertex-disjoint set ; :: thesis: { (H .componentSet()) where H is Element of S : verum } is mutually-disjoint
set M = { (H .componentSet()) where H is Element of S : verum } ;
now :: thesis: for x, y being set st x in { (H .componentSet()) where H is Element of S : verum } & y in { (H .componentSet()) where H is Element of S : verum } & x <> y holds
not x meets y
let x, y be set ; :: thesis: ( x in { (H .componentSet()) where H is Element of S : verum } & y in { (H .componentSet()) where H is Element of S : verum } & x <> y implies not x meets y )
assume x in { (H .componentSet()) where H is Element of S : verum } ; :: thesis: ( y in { (H .componentSet()) where H is Element of S : verum } & x <> y implies not x meets y )
then consider H1 being Element of S such that
A1: x = H1 .componentSet() ;
assume y in { (H .componentSet()) where H is Element of S : verum } ; :: thesis: ( x <> y implies not x meets y )
then consider H2 being Element of S such that
A2: y = H2 .componentSet() ;
assume A3: x <> y ; :: thesis: not x meets y
assume x meets y ; :: thesis: contradiction
then consider z being object such that
A4: ( z in H1 .componentSet() & z in H2 .componentSet() ) by A1, A2, XBOOLE_0:3;
reconsider z = z as set by TARSKI:1;
A5: the_Vertices_of H1 misses the_Vertices_of H2 by A1, A2, A3, Def18;
z c= (the_Vertices_of H1) /\ (the_Vertices_of H2) by A4, XBOOLE_1:19;
then z c= {} by A5, XBOOLE_0:def 7;
hence contradiction by A4; :: thesis: verum
end;
hence { (H .componentSet()) where H is Element of S : verum } is mutually-disjoint by TAXONOM2:def 5; :: thesis: verum