let T be non empty TopSpace; :: thesis: for A, B, C being Subset of T st A c= B & A is_a_component_of C & B is_a_component_of C holds
A = B
let A, B, C be Subset of T; :: thesis: ( A c= B & A is_a_component_of C & B is_a_component_of C implies A = B )
assume that
A1: A c= B and
A2: A is_a_component_of C and
A3: B is_a_component_of C ; :: thesis: A = B
per cases ( C = {} or not C is empty ) ;
suppose C = {} ; :: thesis: A = B
then A4: C = {} T ;
then A = {} by A2, Th6;
hence A = B by A3, A4, Th6; :: thesis: verum
end;
suppose not C is empty ; :: thesis: A = B
then A <> {} by A2, SPRECT_1:4;
hence A = B by A1, A2, A3, GOBOARD9:1, XBOOLE_1:69; :: thesis: verum
end;
end;