let A be Approximation_Space; for X being Subset of A
for x, y being set st x in UAp X & [x,y] in the InternalRel of A holds
y in UAp X
let X be Subset of A; for x, y being set st x in UAp X & [x,y] in the InternalRel of A holds
y in UAp X
let x, y be set ; ( x in UAp X & [x,y] in the InternalRel of A implies y in UAp X )
assume that
A1:
x in UAp X
and
A2:
[x,y] in the InternalRel of A
; y in UAp X
[y,x] in the InternalRel of A
by A2, EQREL_1:6;
then
y in Class ( the InternalRel of A,x)
by EQREL_1:19;
then A3:
Class ( the InternalRel of A,x) = Class ( the InternalRel of A,y)
by A1, EQREL_1:23;
( Class ( the InternalRel of A,x) meets X & y is Element of A )
by A1, A2, Th10, ZFMISC_1:87;
hence
y in UAp X
by A3; verum