let R be non empty transitive RelStr ; :: thesis: for X being Subset of R holds UAp (UAp X) c= UAp X
let X be Subset of R; :: thesis: UAp (UAp X) c= UAp X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp (UAp X) or x in UAp X )
assume x in UAp (UAp X) ; :: thesis: x in UAp X
then x in { y where y is Element of R : Class ( the InternalRel of R,y) meets UAp X } by ROUGHS_1:def 5;
then consider y being Element of R such that
A1: ( y = x & Class ( the InternalRel of R,y) meets UAp X ) ;
consider b being object such that
A2: b in (Class ( the InternalRel of R,y)) /\ (UAp X) by XBOOLE_0:7, XBOOLE_0:def 7, A1;
b in Class ( the InternalRel of R,y) by A2, XBOOLE_0:def 4;
then A3: [y,b] in the InternalRel of R by RELAT_1:169;
b in UAp X by A2, XBOOLE_0:def 4;
then b in { t where t is Element of R : Class ( the InternalRel of R,t) meets X } by ROUGHS_1:def 5;
then consider c being Element of R such that
A4: ( c = b & Class ( the InternalRel of R,c) meets X ) ;
consider d being object such that
A5: d in (Class ( the InternalRel of R,c)) /\ X by XBOOLE_0:7, A4, XBOOLE_0:def 7;
AA: ( d in Class ( the InternalRel of R,c) & d in X ) by XBOOLE_0:def 4, A5;
A6: ( [c,d] in the InternalRel of R & d in X ) by RELAT_1:169, AA;
( [y,d] in the InternalRel of R & d in X ) by ORDERS_2:def 3, RELAT_2:def 8, A6, A3, A4;
then ( d in Im ( the InternalRel of R,y) & d in X ) by RELAT_1:169;
then d in (Class ( the InternalRel of R,y)) /\ X by XBOOLE_0:def 4;
then Class ( the InternalRel of R,y) meets X by XBOOLE_0:def 7;
then y in { t where t is Element of R : Class ( the InternalRel of R,t) meets X } ;
hence x in UAp X by A1, ROUGHS_1:def 5; :: thesis: verum