let R be non empty finite negative_alliance RelStr ; :: thesis: for x being Element of R holds (UAp R) . (((UAp R) . {x}) `) c= ((UAp R) . {x}) `

let x be Element of R; :: thesis: (UAp R) . (((UAp R) . {x}) `) c= ((UAp R) . {x}) `

set H = UAp R;

set L = Flip (UAp R);

w1: (UAp R) . {} = {} by UApEmpty;

w5: for X, Y being Subset of R holds (UAp R) . (X \/ Y) = ((UAp R) . X) \/ ((UAp R) . Y) by UApAdditive;

set RR = GeneratedRelStr (UAp R);

w3: UAp R = UAp (GeneratedRelStr (UAp R)) by KeyTheorem, w1, w5, ROUGHS_4:def 9;

WZ: the InternalRel of (GeneratedRelStr (UAp R)) = the InternalRel of R by Corr3A, w3;

W1: the InternalRel of R is_negative_alliance_in the carrier of R by DefNA;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (UAp R) . (((UAp R) . {x}) `) or y in ((UAp R) . {x}) ` )

assume w2: y in (UAp R) . (((UAp R) . {x}) `) ; :: thesis: y in ((UAp R) . {x}) `

reconsider Hx = ((UAp R) . {x}) ` as Subset of R ;

y in UAp Hx by w2, ROUGHS_2:def 11;

then consider z being object such that

O1: ( z in Class ( the InternalRel of R,y) & z in Hx ) by XBOOLE_0:3, ROUGHS_2:7;

p1: [y,z] in the InternalRel of R by O1, RELAT_1:169;

reconsider zz = z, yy = y as Element of (GeneratedRelStr (UAp R)) by O1, w2;

reconsider xx = x as Element of (GeneratedRelStr (UAp R)) ;

not zz in (UAp R) . {x} by O1, XBOOLE_0:def 5;

then p2: not [zz,x] in the InternalRel of (GeneratedRelStr (UAp R)) by GRDef;

set W = the carrier of R;

set I = the InternalRel of R;

not [yy,xx] in the InternalRel of R by W1, WZ, p2, p1;

then not yy in (UAp R) . {xx} by GRDef, WZ;

hence y in ((UAp R) . {x}) ` by XBOOLE_0:def 5; :: thesis: verum

let x be Element of R; :: thesis: (UAp R) . (((UAp R) . {x}) `) c= ((UAp R) . {x}) `

set H = UAp R;

set L = Flip (UAp R);

w1: (UAp R) . {} = {} by UApEmpty;

w5: for X, Y being Subset of R holds (UAp R) . (X \/ Y) = ((UAp R) . X) \/ ((UAp R) . Y) by UApAdditive;

set RR = GeneratedRelStr (UAp R);

w3: UAp R = UAp (GeneratedRelStr (UAp R)) by KeyTheorem, w1, w5, ROUGHS_4:def 9;

WZ: the InternalRel of (GeneratedRelStr (UAp R)) = the InternalRel of R by Corr3A, w3;

W1: the InternalRel of R is_negative_alliance_in the carrier of R by DefNA;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (UAp R) . (((UAp R) . {x}) `) or y in ((UAp R) . {x}) ` )

assume w2: y in (UAp R) . (((UAp R) . {x}) `) ; :: thesis: y in ((UAp R) . {x}) `

reconsider Hx = ((UAp R) . {x}) ` as Subset of R ;

y in UAp Hx by w2, ROUGHS_2:def 11;

then consider z being object such that

O1: ( z in Class ( the InternalRel of R,y) & z in Hx ) by XBOOLE_0:3, ROUGHS_2:7;

p1: [y,z] in the InternalRel of R by O1, RELAT_1:169;

reconsider zz = z, yy = y as Element of (GeneratedRelStr (UAp R)) by O1, w2;

reconsider xx = x as Element of (GeneratedRelStr (UAp R)) ;

not zz in (UAp R) . {x} by O1, XBOOLE_0:def 5;

then p2: not [zz,x] in the InternalRel of (GeneratedRelStr (UAp R)) by GRDef;

set W = the carrier of R;

set I = the InternalRel of R;

not [yy,xx] in the InternalRel of R by W1, WZ, p2, p1;

then not yy in (UAp R) . {xx} by GRDef, WZ;

hence y in ((UAp R) . {x}) ` by XBOOLE_0:def 5; :: thesis: verum