let R be non empty finite positive_alliance RelStr ; :: thesis: for x being Element of R holds ((UAp R) . {x}) ` c= (UAp R) . (((UAp R) . {x}) `)
let x be Element of R; :: thesis: ((UAp R) . {x}) ` c= (UAp R) . (((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;
WW: for x, y being Element of (GeneratedRelStr (UAp R)) holds
( [x,y] in the InternalRel of (GeneratedRelStr (UAp R)) iff x in (UAp R) . {y} ) by GRDef;
WZ: the InternalRel of (GeneratedRelStr (UAp R)) = the InternalRel of R by Corr3A, w3;
W1: the InternalRel of R is_positive_alliance_in the carrier of R by DefPA;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ((UAp R) . {x}) ` or y in (UAp R) . (((UAp R) . {x}) `) )
assume w2: y in ((UAp R) . {x}) ` ; :: thesis: y in (UAp R) . (((UAp R) . {x}) `)
then w1: not y in (UAp R) . {x} by XBOOLE_0:def 5;
reconsider xx = x, yy = y as Element of (GeneratedRelStr (UAp R)) by w2;
not [yy,xx] in the InternalRel of (GeneratedRelStr (UAp R)) by w1, GRDef;
then consider z being object such that
W2: ( z in the carrier of R & [y,z] in the InternalRel of R ) and
W3: not [z,x] in the InternalRel of (GeneratedRelStr (UAp R)) by W1, WZ;
reconsider zz = z as Element of (GeneratedRelStr (UAp R)) by W2;
W5: yy in (UAp R) . {zz} by W2, GRDef, WZ;
j1: {z} c= the carrier of R by ZFMISC_1:31, W2;
w6: z in ((UAp R) . {x}) ` by W3, WW, SUBSET_1:29, W2;
for X, Y being Subset of R holds (UAp R) . (X \/ Y) = ((UAp R) . X) \/ ((UAp R) . Y) by UApAdditive;
then UAp R is \/-preserving by ROUGHS_4:def 9;
then (UAp R) . {z} c= (UAp R) . (((UAp R) . {x}) `) by w6, j1, ROUGHS_4:def 8, ZFMISC_1:31;
hence y in (UAp R) . (((UAp R) . {x}) `) by W5; :: thesis: verum