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