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 A1: ( A is a_union_of_components of GX & B is a_union_of_components of GX ) ; :: thesis: A \ B is a_union_of_components of GX
then consider Fa being Subset-Family of GX such that
A2: ( ( for B2 being Subset of GX st B2 in Fa holds
B2 is_a_component_of GX ) & A = union Fa ) by Def2;
consider Fb being Subset-Family of GX such that
A3: ( ( for B3 being Subset of GX st B3 in Fb holds
B3 is_a_component_of GX ) & B = union Fb ) by A1, Def2;
reconsider Fd = Fa \ Fb as Subset-Family of GX ;
A4: A \ B = union Fd

proof

A5: A \ B c= union Fd

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A \ B or x in union Fd )
assume A6: x in A \ B ; :: thesis: x in union Fd
then ( x in A & not x in B ) by XBOOLE_0:def 5;
then consider X being set such that
A7: ( x in X & X in Fa ) by A2, TARSKI:def 4;
reconsider A2 = X as Subset of GX by A7;

now

assume A2 in Fb ; :: thesis: contradiction
then A2 c= B by A3, ZFMISC_1:92;
hence contradiction by A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

then A2 in Fd by A7, XBOOLE_0:def 5;
hence x in union Fd by A7, TARSKI:def 4; :: thesis: verum

end;

union Fd c= A \ B

proof

let x be set ; :: 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 & X in Fd ) by TARSKI:def 4;
A9: ( X in Fa & not X in Fb ) by A8, XBOOLE_0:def 5;
reconsider A2 = X as Subset of GX by A8;
A10: A2 is_a_component_of GX by A2, A9;
A11: A2 c= A by A2, A9, ZFMISC_1:92;

now

assume x in B ; :: thesis: contradiction
then consider Y3 being set such that
A12: ( x in Y3 & Y3 in Fb ) by A3, TARSKI:def 4;
reconsider B3 = Y3 as Subset of GX by A12;
A13: B3 is_a_component_of GX by A3, A12;
A2 /\ B3 <> {} by A8, A12, XBOOLE_0:def 4;
then A2 meets B3 by XBOOLE_0:def 7;
hence contradiction by A9, A10, A12, A13, CONNSP_1:37; :: thesis: verum

end;

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

end;

hence A \ B = union Fd by A5, XBOOLE_0:def 10; :: thesis: verum

end;

for B4 being Subset of GX st B4 in Fd holds
B4 is_a_component_of GX

proof

let B4 be Subset of GX; :: thesis: ( B4 in Fd implies B4 is_a_component_of GX )
assume B4 in Fd ; :: thesis: B4 is_a_component_of GX
then B4 in Fa by XBOOLE_0:def 5;
hence B4 is_a_component_of GX by A2; :: thesis: verum

end;

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