reconsider R = {} [:{} ,{} :] as Relation of {} ;
RelStr(# {} ,R #) in fin_RelStr

proof

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

end;

hence not fin_RelStr is empty ; :: thesis: verum