set R = RelStr(# {{}},(id {{}}) #);
take RelStr(# {{}},(id {{}}) #) ; :: thesis: ( RelStr(# {{}},(id {{}}) #) is strict & RelStr(# {{}},(id {{}}) #) is finite )
thus ( RelStr(# {{}},(id {{}}) #) is strict & RelStr(# {{}},(id {{}}) #) is finite ) ; :: thesis: verum