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

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