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:12;
then y in Class the InternalRel of A,x by EQREL_1:27;
then A3: Class the InternalRel of A,x = Class the InternalRel of A,y by A1, EQREL_1:31;
( Class the InternalRel of A,x meets X & y is Element of A ) by A1, A2, Th10, ZFMISC_1:106;
hence y in UAp X by A3; :: thesis: verum