let S be non empty Graph-membered connected set ; :: thesis: { (H .componentSet()) where H is Element of S : verum } = SmallestPartition (the_Vertices_of S)
set M1 = { (H .componentSet()) where H is Element of S : verum } ;
set M2 = { {X} where X is Element of the_Vertices_of S : verum } ;
now :: thesis: for x being object holds
( ( x in { (H .componentSet()) where H is Element of S : verum } implies x in { {X} where X is Element of the_Vertices_of S : verum } ) & ( x in { {X} where X is Element of the_Vertices_of S : verum } implies x in { (H .componentSet()) where H is Element of S : verum } ) )
let x be object ; :: thesis: ( ( x in { (H .componentSet()) where H is Element of S : verum } implies x in { {X} where X is Element of the_Vertices_of S : verum } ) & ( x in { {X} where X is Element of the_Vertices_of S : verum } implies x in { (H .componentSet()) where H is Element of S : verum } ) )
hereby :: thesis: ( x in { {X} where X is Element of the_Vertices_of S : verum } implies x in { (H .componentSet()) where H is Element of S : verum } )
assume x in { (H .componentSet()) where H is Element of S : verum } ; :: thesis: x in { {X} where X is Element of the_Vertices_of S : verum }
then consider H being Element of S such that
A1: x = H .componentSet() ;
A2: x = {(the_Vertices_of H)} by A1, GLIB_002:25;
the_Vertices_of H in the_Vertices_of S by GLIB_014:def 14;
hence x in { {X} where X is Element of the_Vertices_of S : verum } by A2; :: thesis: verum
end;
assume x in { {X} where X is Element of the_Vertices_of S : verum } ; :: thesis: x in { (H .componentSet()) where H is Element of S : verum }
then consider X being Element of the_Vertices_of S such that
A3: x = {X} ;
consider H being _Graph such that
A4: ( H in S & X = the_Vertices_of H ) by GLIB_014:def 14;
reconsider H = H as Element of S by A4;
x = H .componentSet() by A3, A4, GLIB_002:25;
hence x in { (H .componentSet()) where H is Element of S : verum } ; :: thesis: verum
end;
then { (H .componentSet()) where H is Element of S : verum } = { {X} where X is Element of the_Vertices_of S : verum } by TARSKI:2;
hence { (H .componentSet()) where H is Element of S : verum } = SmallestPartition (the_Vertices_of S) by EQREL_1:37; :: thesis: verum