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

proof

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;

A13: now :: thesis: not x in B

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;

A2 c= A by A4, A11, ZFMISC_1:74;
hence x in A \ B by A8, A13, XBOOLE_0:def 5; :: thesis: verum

end;

A17: for B4 being Subset of GX st B4 in Fd holds
B4 is a_component

proof

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;

A \ B c= union Fd

proof

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;

now :: thesis: not A2 in Fb

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 in Fd by A20, XBOOLE_0:def 5;
hence x in union Fd by A19, TARSKI:def 4; :: thesis: verum

end;

then A \ B = union Fd by A7;
hence A \ B is a_union_of_components of GX by A17, Def2; :: thesis: verum