let T be TopSpace; :: thesis: for A being Subset of holds
( A is_a_component_of {} T iff A is empty )
let A be Subset of ; :: thesis: ( A is_a_component_of {} T iff A is empty )
thus ( A is_a_component_of {} T implies A is empty ) by SPRECT_1:7, XBOOLE_1:3; :: thesis: ( A is empty implies A is_a_component_of {} T )
assume A1: A is empty ; :: thesis: A is_a_component_of {} T
then reconsider B = A as Subset of by XBOOLE_1:2;
for C being Subset of st C is connected & B c= C holds
B = C by A1, XBOOLE_1:3;
then B is_a_component_of T | ({} T) by A1, CONNSP_1:def 5;
hence A is_a_component_of {} T by CONNSP_1:def 6; :: thesis: verum