let T be TopSpace; :: thesis: for A being Subset of T holds
( A is_a_component_of {} T iff A is empty )
let A be Subset of T; :: 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:5, 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 (T | ({} T)) by XBOOLE_1:2;
for C being Subset of (T | ({} T)) st C is connected & B c= C holds
B = C by A1;
then B is a_component by A1, CONNSP_1:def 5;
hence A is_a_component_of {} T by CONNSP_1:def 6; :: thesis: verum