let R be non empty mediate RelStr ; for X being Subset of R holds UAp X c= UAp (UAp X)
let X be Subset of R; UAp X c= UAp (UAp X)
let y be object ; TARSKI:def 3 ( not y in UAp X or y in UAp (UAp X) )
assume
y in UAp X
; 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; verum