let A be Approximation_Space; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum