let R be non empty mediate RelStr ; :: thesis: for X being Subset of R holds UAp X c= UAp (UAp X)
let X be Subset of R; :: thesis: UAp X c= UAp (UAp X)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in UAp X or y in UAp (UAp X) )
assume y in UAp X ; :: thesis: y in UAp (UAp X)
then consider t being Element of R such that
A1: ( t = y & Class ( the InternalRel of R,t) meets X ) ;
ex w being object st w in (Class ( the InternalRel of R,t)) /\ X by A1, XBOOLE_0:def 1;
then consider w being Element of the carrier of R such that
A2: w in (Class ( the InternalRel of R,t)) /\ X ;
A3: ( w in Class ( the InternalRel of R,t) & w in X ) by XBOOLE_0:def 4, A2;
then [t,w] in the InternalRel of R by RELAT_1:169;
then consider z being object such that
A4: ( z in the carrier of R & [t,z] in the InternalRel of R & [z,w] in the InternalRel of R ) by Def5, Def7;
reconsider z = z as Element of R by A4;
A5: ( z in Class ( the InternalRel of R,t) & w in Class ( the InternalRel of R,z) ) by A4, RELAT_1:169;
then Class ( the InternalRel of R,z) meets X by A3, XBOOLE_0:def 4;
then A6: z in { x where x is Element of R : Class ( the InternalRel of R,x) meets X } ;
A7: UAp {z} c= UAp (UAp X) by Th15, A6, ZFMISC_1:31;
z in {z} by TARSKI:def 1;
then Class ( the InternalRel of R,t) meets {z} by A5, XBOOLE_0:def 4;
then t in { x where x is Element of R : Class ( the InternalRel of R,x) meets {z} } ;
hence y in UAp (UAp X) by A1, A7; :: thesis: verum