[:{0},{0}:] c= [:{0},{0}:] ;
then reconsider R = [:{0},{0}:] as Relation of {0} ;
RelStr(# {0},R #) in fin_RelStr_sp

proof

set X = RelStr(# {0},R #);
A1: the carrier of RelStr(# {0},R #) in FinSETS by CLASSES2:56, CLASSES2:57;
thus RelStr(# {0},R #) in fin_RelStr_sp by A1, Def5; :: thesis: verum

end;

hence not fin_RelStr_sp is empty ; :: thesis: verum