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

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