let GX be non empty TopSpace; :: thesis: for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ) holds
meet Fu is a_union_of_components of GX
let Fu be Subset-Family of GX; :: thesis: ( ( for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ) implies meet Fu is a_union_of_components of GX )
assume A1: for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ; :: thesis: meet Fu is a_union_of_components of GX

now :: thesis: ( ( Fu <> {} & meet Fu is a_union_of_components of GX ) or ( Fu = {} & meet Fu is a_union_of_components of GX ) )

per cases ( Fu <> {} or Fu = {} ) ;

case A2: Fu <> {} ; :: thesis: meet Fu is a_union_of_components of GX

{ B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B c= A2 ) ) } c= bool the carrier of GX

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B c= A2 ) ) } or x in bool the carrier of GX )
assume x in { B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B c= A2 ) ) } ; :: thesis: x in bool the carrier of GX
then ex B being Subset of GX st
( x = B & B is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B c= A2 ) ) ;
hence x in bool the carrier of GX ; :: thesis: verum

end;

then reconsider F1 = { B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B c= A2 ) ) } as Subset-Family of GX ;
A3: meet Fu c= union F1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet Fu or x in union F1 )
consider Y2 being object such that
A4: Y2 in Fu by A2, XBOOLE_0:def 1;
reconsider Y2 = Y2 as set by TARSKI:1;
reconsider B2 = Y2 as Subset of GX by A4;
B2 is a_union_of_components of GX by A1, A4;
then consider F being Subset-Family of GX such that
A5: for B being Subset of GX st B in F holds
B is a_component and
A6: B2 = union F by Def2;
assume A7: x in meet Fu ; :: thesis: x in union F1
then x in Y2 by A4, SETFAM_1:def 1;
then consider Y3 being set such that
A8: x in Y3 and
A9: Y3 in F by A6, TARSKI:def 4;
reconsider B3 = Y3 as Subset of GX by A9;
A10: for A2 being Subset of GX st A2 in Fu holds
B3 c= A2

proof

reconsider p = x as Point of GX by A7;
let A2 be Subset of GX; :: thesis: ( A2 in Fu implies B3 c= A2 )
assume A11: A2 in Fu ; :: thesis: B3 c= A2
then x in A2 by A7, SETFAM_1:def 1;
then Component_of p c= A2 by A1, A11, Th21;
hence B3 c= A2 by A5, A8, A9, CONNSP_1:41; :: thesis: verum

end;

B3 is a_component by A5, A9;
then Y3 in F1 by A10;
hence x in union F1 by A8, TARSKI:def 4; :: thesis: verum

end;

A12: for B being Subset of GX st B in F1 holds
B is a_component

proof

let B be Subset of GX; :: thesis: ( B in F1 implies B is a_component )
assume B in F1 ; :: thesis: B is a_component
then ex B1 being Subset of GX st
( B = B1 & B1 is a_component & ( for A2 being Subset of GX st A2 in Fu holds
B1 c= A2 ) ) ;
hence B is a_component ; :: thesis: verum

end;

union F1 c= meet Fu

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union F1 or x in meet Fu )
assume x in union F1 ; :: thesis: x in meet Fu
then consider X being set such that
A13: x in X and
A14: X in F1 by TARSKI:def 4;
consider B being Subset of GX such that
A15: X = B and
B is a_component and
A16: for A2 being Subset of GX st A2 in Fu holds
B c= A2 by A14;
for Y being set st Y in Fu holds
x in Y

proof

let Y be set ; :: thesis: ( Y in Fu implies x in Y )
assume Y in Fu ; :: thesis: x in Y
then B c= Y by A16;
hence x in Y by A13, A15; :: thesis: verum

end;

hence x in meet Fu by A2, SETFAM_1:def 1; :: thesis: verum

end;

then meet Fu = union F1 by A3;
hence meet Fu is a_union_of_components of GX by A12, Def2; :: thesis: verum

end;

case Fu = {} ; :: thesis: meet Fu is a_union_of_components of GX

then meet Fu = {} GX by SETFAM_1:def 1;
hence meet Fu is a_union_of_components of GX by Th19; :: thesis: verum

end;

end;

end;

hence meet Fu is a_union_of_components of GX ; :: thesis: verum