let R be RelStr ; :: thesis: ( R in fin_RelStr_sp implies the carrier of R in FinSETS )
assume R in fin_RelStr_sp ; :: thesis: the carrier of R in FinSETS
then ex S being strict RelStr st
( R = S & the carrier of S in FinSETS ) by Def4;
hence the carrier of R in FinSETS ; :: thesis: verum