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