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

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