RelStr(# {},({} ({},{})) #) in fin_RelStr

proof

set X = RelStr(# {},({} ({},{})) #);
the carrier of RelStr(# {},({} ({},{})) #) in FinSETS by CLASSES1:2, CLASSES2:def 2;
hence RelStr(# {},({} ({},{})) #) in fin_RelStr by Def4; :: thesis: verum

end;

hence not fin_RelStr is empty ; :: thesis: verum