let GX be non empty TopSpace; :: thesis: for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds

A \ B is a_union_of_components of GX

let A, B be Subset of GX; :: thesis: ( A is a_union_of_components of GX & B is a_union_of_components of GX implies A \ B is a_union_of_components of GX )

assume that

A1: A is a_union_of_components of GX and

A2: B is a_union_of_components of GX ; :: thesis: A \ B is a_union_of_components of GX

consider Fa being Subset-Family of GX such that

A3: for B2 being Subset of GX st B2 in Fa holds

B2 is a_component and

A4: A = union Fa by A1, Def2;

consider Fb being Subset-Family of GX such that

A5: for B3 being Subset of GX st B3 in Fb holds

B3 is a_component and

A6: B = union Fb by A2, Def2;

reconsider Fd = Fa \ Fb as Subset-Family of GX ;

A7: union Fd c= A \ B

B4 is a_component

hence A \ B is a_union_of_components of GX by A17, Def2; :: thesis: verum

A \ B is a_union_of_components of GX

let A, B be Subset of GX; :: thesis: ( A is a_union_of_components of GX & B is a_union_of_components of GX implies A \ B is a_union_of_components of GX )

assume that

A1: A is a_union_of_components of GX and

A2: B is a_union_of_components of GX ; :: thesis: A \ B is a_union_of_components of GX

consider Fa being Subset-Family of GX such that

A3: for B2 being Subset of GX st B2 in Fa holds

B2 is a_component and

A4: A = union Fa by A1, Def2;

consider Fb being Subset-Family of GX such that

A5: for B3 being Subset of GX st B3 in Fb holds

B3 is a_component and

A6: B = union Fb by A2, Def2;

reconsider Fd = Fa \ Fb as Subset-Family of GX ;

A7: union Fd c= A \ B

proof

A17:
for B4 being Subset of GX st B4 in Fd holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union Fd or x in A \ B )

assume x in union Fd ; :: thesis: x in A \ B

then consider X being set such that

A8: x in X and

A9: X in Fd by TARSKI:def 4;

reconsider A2 = X as Subset of GX by A9;

A10: not X in Fb by A9, XBOOLE_0:def 5;

A11: X in Fa by A9, XBOOLE_0:def 5;

then A12: A2 is a_component by A3;

hence x in A \ B by A8, A13, XBOOLE_0:def 5; :: thesis: verum

end;assume x in union Fd ; :: thesis: x in A \ B

then consider X being set such that

A8: x in X and

A9: X in Fd by TARSKI:def 4;

reconsider A2 = X as Subset of GX by A9;

A10: not X in Fb by A9, XBOOLE_0:def 5;

A11: X in Fa by A9, XBOOLE_0:def 5;

then A12: A2 is a_component by A3;

A13: now :: thesis: not x in B

A2 c= A
by A4, A11, ZFMISC_1:74;assume
x in B
; :: thesis: contradiction

then consider Y3 being set such that

A14: x in Y3 and

A15: Y3 in Fb by A6, TARSKI:def 4;

reconsider B3 = Y3 as Subset of GX by A15;

A2 /\ B3 <> {} by A8, A14, XBOOLE_0:def 4;

then A16: A2 meets B3 ;

B3 is a_component by A5, A15;

hence contradiction by A10, A12, A15, A16, CONNSP_1:35; :: thesis: verum

end;then consider Y3 being set such that

A14: x in Y3 and

A15: Y3 in Fb by A6, TARSKI:def 4;

reconsider B3 = Y3 as Subset of GX by A15;

A2 /\ B3 <> {} by A8, A14, XBOOLE_0:def 4;

then A16: A2 meets B3 ;

B3 is a_component by A5, A15;

hence contradiction by A10, A12, A15, A16, CONNSP_1:35; :: thesis: verum

hence x in A \ B by A8, A13, XBOOLE_0:def 5; :: thesis: verum

B4 is a_component

proof

A \ B c= union Fd
let B4 be Subset of GX; :: thesis: ( B4 in Fd implies B4 is a_component )

assume B4 in Fd ; :: thesis: B4 is a_component

then B4 in Fa by XBOOLE_0:def 5;

hence B4 is a_component by A3; :: thesis: verum

end;assume B4 in Fd ; :: thesis: B4 is a_component

then B4 in Fa by XBOOLE_0:def 5;

hence B4 is a_component by A3; :: thesis: verum

proof

then
A \ B = union Fd
by A7;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A \ B or x in union Fd )

assume A18: x in A \ B ; :: thesis: x in union Fd

then x in A by XBOOLE_0:def 5;

then consider X being set such that

A19: x in X and

A20: X in Fa by A4, TARSKI:def 4;

reconsider A2 = X as Subset of GX by A20;

hence x in union Fd by A19, TARSKI:def 4; :: thesis: verum

end;assume A18: x in A \ B ; :: thesis: x in union Fd

then x in A by XBOOLE_0:def 5;

then consider X being set such that

A19: x in X and

A20: X in Fa by A4, TARSKI:def 4;

reconsider A2 = X as Subset of GX by A20;

now :: thesis: not A2 in Fb

then
A2 in Fd
by A20, XBOOLE_0:def 5;assume
A2 in Fb
; :: thesis: contradiction

then A2 c= B by A6, ZFMISC_1:74;

hence contradiction by A18, A19, XBOOLE_0:def 5; :: thesis: verum

end;then A2 c= B by A6, ZFMISC_1:74;

hence contradiction by A18, A19, XBOOLE_0:def 5; :: thesis: verum

hence x in union Fd by A19, TARSKI:def 4; :: thesis: verum

hence A \ B is a_union_of_components of GX by A17, Def2; :: thesis: verum