let GX be TopSpace; :: thesis: for V being Subset of GX st ex A being Subset of GX st
( A is connected & V c= A ) holds
V c= Component_of V
let V be Subset of GX; :: thesis: ( ex A being Subset of GX st
( A is connected & V c= A ) implies V c= Component_of V )
given A being Subset of GX such that A1: ( A is connected & V c= A ) ; :: thesis: V c= Component_of V
consider F being Subset-Family of GX such that
A2: for A being Subset of GX holds
( A in F iff ( A is connected & V c= A ) ) and
A3: Component_of V = union F by Def1;
A4: for A being set st A in F holds
V c= A by A2;
F <> {} by A1, A2;
then A5: V c= meet F by A4, SETFAM_1:5;
meet F c= union F by SETFAM_1:2;
hence V c= Component_of V by A3, A5; :: thesis: verum