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