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