let R be non empty reflexive RelStr ; :: thesis: for x being Element of R holds x in Class ( the InternalRel of R,x)
let x be Element of R; :: thesis: x in Class ( the InternalRel of R,x)
A1: x in field the InternalRel of R by Th1;
A2: x in {x} by TARSKI:def 1;
[x,x] in the InternalRel of R by A1, RELAT_2:def 1, RELAT_2:def 9;
hence x in Class ( the InternalRel of R,x) by RELAT_1:def 13, A2; :: thesis: verum