let R be non empty total RelStr ; :: thesis: for x being Element of R holds x in field the InternalRel of R
let x be Element of R; :: thesis: x in field the InternalRel of R
dom the InternalRel of R = the carrier of R by PARTFUN1:def 2;
hence x in field the InternalRel of R by XBOOLE_0:def 3; :: thesis: verum