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 )
set x = the Point of FT;
{} c= { the Point of FT} ;
hence ( A is_a_component_of FT implies A <> {} FT ) ; :: thesis: verum