let R be RelStr ; :: thesis: for x being Element of R
for y being set st y in component x holds
[x,y] in EqCl the InternalRel of R
let x be Element of R; :: thesis: for y being set st y in component x holds
[x,y] in EqCl the InternalRel of R
let y be set ; :: thesis: ( y in component x implies [x,y] in EqCl the InternalRel of R )
set IR = the InternalRel of R;
assume y in component x ; :: thesis: [x,y] in EqCl the InternalRel of R
then [y,x] in EqCl the InternalRel of R by EQREL_1:19;
hence [x,y] in EqCl the InternalRel of R by EQREL_1:6; :: thesis: verum