[:{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: ( not the carrier of RelStr(# {0 },R #) is empty & the carrier of RelStr(# {0 },R #) is trivial ) by REALSET1:def 4;
the carrier of RelStr(# {0 },R #) in FinSETS by CLASSES2:62, CLASSES2:63;
hence RelStr(# {0 },R #) in fin_RelStr_sp by A1, Def5; :: thesis: verum

end;

hence not fin_RelStr_sp is empty ; :: thesis: verum