let T be non empty TopSpace; :: thesis: for A being non empty Subset of T
for B1, B2, C1, C2 being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A & C1 is_a_component_of A & C2 is_a_component_of A & B1 \/ B2 = A & C1 \/ C2 = A holds
{B1,B2} = {C1,C2}
let A be non empty Subset of T; :: thesis: for B1, B2, C1, C2 being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A & C1 is_a_component_of A & C2 is_a_component_of A & B1 \/ B2 = A & C1 \/ C2 = A holds
{B1,B2} = {C1,C2}
let B1, B2, C1, C2 be Subset of T; :: thesis: ( B1 is_a_component_of A & B2 is_a_component_of A & C1 is_a_component_of A & C2 is_a_component_of A & B1 \/ B2 = A & C1 \/ C2 = A implies {B1,B2} = {C1,C2} )
assume that
A1: B1 is_a_component_of A and
A2: B2 is_a_component_of A and
A3: C1 is_a_component_of A and
A4: C2 is_a_component_of A and
A5: B1 \/ B2 = A and
A6: C1 \/ C2 = A ; :: thesis: {B1,B2} = {C1,C2}

now :: thesis: for x being object holds
( x in {B1,B2} iff ( x = C1 or x = C2 ) )

let x be object ; :: thesis: ( x in {B1,B2} iff ( x = C1 or x = C2 ) )
( ( ( not x = B1 & not x = B2 ) or x = C1 or x = C2 ) & ( ( not x = C1 & not x = C2 ) or x = B1 or x = B2 ) ) by A1, A2, A3, A4, A5, A6, Th6;
hence ( x in {B1,B2} iff ( x = C1 or x = C2 ) ) by TARSKI:def 2; :: thesis: verum

end;

hence {B1,B2} = {C1,C2} by TARSKI:def 2; :: thesis: verum