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

proof

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

end;

hence not fin_RelStr is empty ; :: thesis: verum