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

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 ) )end;

hence
meet Fu is a_union_of_components of GX
; :: thesis: verumper cases
( Fu <> {} or Fu = {} )
;

end;

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

B c= A2 ) ) } as Subset-Family of GX ;

A3: meet Fu c= union F1

B is a_component

hence meet Fu is a_union_of_components of GX by A12, Def2; :: thesis: verum

end;B c= A2 ) ) } c= bool the carrier of GX

proof

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
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;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

B c= A2 ) ) } as Subset-Family of GX ;

A3: meet Fu c= union F1

proof

A12:
for B being Subset of GX st B in F1 holds
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

then Y3 in F1 by A10;

hence x in union F1 by A8, TARSKI:def 4; :: thesis: verum

end;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

B3 is a_component
by A5, A9;
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;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

then Y3 in F1 by A10;

hence x in union F1 by A8, TARSKI:def 4; :: thesis: verum

B is a_component

proof

union F1 c= meet Fu
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;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

proof

then
meet Fu = union F1
by A3;
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

end;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

hence
x in meet Fu
by A2, SETFAM_1:def 1; :: thesis: verum
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;assume Y in Fu ; :: thesis: x in Y

then B c= Y by A16;

hence x in Y by A13, A15; :: thesis: verum

hence meet Fu is a_union_of_components of GX by A12, Def2; :: thesis: verum

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;hence meet Fu is a_union_of_components of GX by Th19; :: thesis: verum