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

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