let FT be non empty RelStr ; :: thesis: for A being Subset of st A is_a_component_of FT holds
A <> {} FT
let A be Subset of ; :: thesis: ( A is_a_component_of FT implies A <> {} FT )
consider x being Point of ;
{} c= {x} by XBOOLE_1:2;
hence ( A is_a_component_of FT implies A <> {} FT ) by Def4; :: thesis: verum