[:{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:62, CLASSES2:63;
thus RelStr(# {0 },R #) in fin_RelStr_sp by A1, Def5; :: thesis: verum

end;

hence not fin_RelStr_sp is empty ; :: thesis: verum