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

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