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 ;
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 ;
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 ;
A11: X in Fa by ;
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 ;
reconsider B3 = Y3 as Subset of GX by A15;
A2 /\ B3 <> {} by ;
then A16: A2 meets B3 ;
B3 is a_component by ;
hence contradiction by A10, A12, A15, A16, CONNSP_1:35; :: thesis: verum
end;
A2 c= A by ;
hence x in A \ B by ; :: 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 ;
reconsider A2 = X as Subset of GX by A20;
now :: thesis: not A2 in Fbend;
then A2 in Fd by ;
hence x in union Fd by ; :: thesis: verum
end;
then A \ B = union Fd by A7;
hence A \ B is a_union_of_components of GX by ; :: thesis: verum