let G2 be _Graph; :: thesis: for v1, v2 being Vertex of G2 st not v2 in G2 .reachableFrom v1 holds
not (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) in G2 .componentSet()
let v1, v2 be Vertex of G2; :: thesis: ( not v2 in G2 .reachableFrom v1 implies not (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) in G2 .componentSet() )
assume A1: not v2 in G2 .reachableFrom v1 ; :: thesis: not (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) in G2 .componentSet()
set V1 = G2 .reachableFrom v1;
set V2 = G2 .reachableFrom v2;
reconsider C = G2 .componentSet() as a_partition of the_Vertices_of G2 by Th23;
A2: ( G2 .reachableFrom v1 in C & G2 .reachableFrom v2 in C ) by GLIB_002:def 8;
A3: G2 .reachableFrom v1 misses G2 .reachableFrom v2 by A1, Th22;
assume (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) in G2 .componentSet() ; :: thesis: contradiction
per cases then ( (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) = G2 .reachableFrom v1 or (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) misses G2 .reachableFrom v1 ) by A2, EQREL_1:def 4;
suppose (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) = G2 .reachableFrom v1 ; :: thesis: contradiction
then G2 .reachableFrom v2 c= G2 .reachableFrom v1 by XBOOLE_1:11;
hence contradiction by A3, XBOOLE_1:63, XBOOLE_1:66; :: thesis: verum
end;
suppose (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) misses G2 .reachableFrom v1 ; :: thesis: contradiction
then G2 .reachableFrom v1 misses G2 .reachableFrom v1 by XBOOLE_1:70;
hence contradiction ; :: thesis: verum
end;
end;