let G be _Graph; :: thesis: G .componentSet() is a_partition of the_Vertices_of G
set V = the_Vertices_of G;
A1: union (G .componentSet()) = the_Vertices_of G by GLIB_002:24;
for A being Subset of (the_Vertices_of G) st A in G .componentSet() holds
( A <> {} & ( for B being Subset of (the_Vertices_of G) holds
( not B in G .componentSet() or A = B or A misses B ) ) )
proof
let A be Subset of (the_Vertices_of G); :: thesis: ( A in G .componentSet() implies ( A <> {} & ( for B being Subset of (the_Vertices_of G) holds
( not B in G .componentSet() or A = B or A misses B ) ) ) )
assume A in G .componentSet() ; :: thesis: ( A <> {} & ( for B being Subset of (the_Vertices_of G) holds
( not B in G .componentSet() or A = B or A misses B ) ) )
then consider v being Vertex of G such that
A2: A = G .reachableFrom v by GLIB_002:def 8;
thus A <> {} by A2; :: thesis: for B being Subset of (the_Vertices_of G) holds
( not B in G .componentSet() or A = B or A misses B )
let B be Subset of (the_Vertices_of G); :: thesis: ( not B in G .componentSet() or A = B or A misses B )
assume B in G .componentSet() ; :: thesis: ( A = B or A misses B )
then consider w being Vertex of G such that
A3: B = G .reachableFrom w by GLIB_002:def 8;
per cases ( v in G .reachableFrom w or not v in G .reachableFrom w ) ;
suppose v in G .reachableFrom w ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A2, A3, GLIB_002:12; :: thesis: verum
end;
suppose not v in G .reachableFrom w ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A2, A3, Th22; :: thesis: verum
end;
end;
end;
hence G .componentSet() is a_partition of the_Vertices_of G by A1, EQREL_1:def 4; :: thesis: verum