let R be RelStr ; :: thesis: ( R in fin_RelStr_sp implies the carrier of R in FinSETS )
assume A1: R in fin_RelStr_sp ; :: thesis: the carrier of R in FinSETS
consider S being strict RelStr such that
A2: ( R = S & the carrier of S in FinSETS ) by A1, Def4;
thus the carrier of R in FinSETS by A2; :: thesis: verum