let A be non empty finite set ; :: thesis: for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds (U . X) ` c= U . ((U . X) `) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & U = UAp R )

let U be Function of (bool A),(bool A); :: thesis: ( U . {} = {} & ( for X being Subset of A holds (U . X) ` c= U . ((U . X) `) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & U = UAp R ) )

assume a0: ( U . {} = {} & ( for X being Subset of A holds (U . X) ` c= U . ((U . X) `) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) ) ; :: thesis: ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & U = UAp R )

then consider R being non empty finite RelStr such that

a1: ( the carrier of R = A & LAp R = Flip U & UAp R = U & ( for x, y being Element of R holds

( [x,y] in the InternalRel of R iff x in U . {y} ) ) ) by YaoTh3;

set X = the carrier of R;

set I = the InternalRel of R;

for x, y being object st x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R holds

ex z being object st

( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R )

then R is positive_alliance ;

hence ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & U = UAp R ) by a1; :: thesis: verum

ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & U = UAp R )

let U be Function of (bool A),(bool A); :: thesis: ( U . {} = {} & ( for X being Subset of A holds (U . X) ` c= U . ((U . X) `) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & U = UAp R ) )

assume a0: ( U . {} = {} & ( for X being Subset of A holds (U . X) ` c= U . ((U . X) `) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) ) ; :: thesis: ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & U = UAp R )

then consider R being non empty finite RelStr such that

a1: ( the carrier of R = A & LAp R = Flip U & UAp R = U & ( for x, y being Element of R holds

( [x,y] in the InternalRel of R iff x in U . {y} ) ) ) by YaoTh3;

set X = the carrier of R;

set I = the InternalRel of R;

for x, y being object st x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R holds

ex z being object st

( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R )

proof

then
the InternalRel of R is_positive_alliance_in the carrier of R
;
let x, y be object ; :: thesis: ( x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R implies ex z being object st

( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) )

assume W1: ( x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R ) ; :: thesis: ex z being object st

( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R )

then reconsider xx = x, yy = y as Element of R ;

a3: ((UAp R) . {yy}) ` c= U . (((UAp R) . {yy}) `) by a0, a1;

not xx in (UAp R) . {yy} by W1, a1;

then xx in ((UAp R) . {yy}) ` by XBOOLE_0:def 5;

then xx in (UAp R) . (((UAp R) . {yy}) `) by a3, a1;

then xx in UAp (((UAp R) . {yy}) `) by ROUGHS_2:def 11;

then consider z being object such that

J1: ( z in Class ( the InternalRel of R,xx) & z in ((UAp R) . {yy}) ` ) by XBOOLE_0:3, ROUGHS_2:7;

reconsider zz = z as Element of R by J1;

J2: [xx,zz] in the InternalRel of R by J1, RELAT_1:169;

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

then not [z,y] in the InternalRel of R by a1;

hence ex z being object st

( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) by J2; :: thesis: verum

end;( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) )

assume W1: ( x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R ) ; :: thesis: ex z being object st

( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R )

then reconsider xx = x, yy = y as Element of R ;

a3: ((UAp R) . {yy}) ` c= U . (((UAp R) . {yy}) `) by a0, a1;

not xx in (UAp R) . {yy} by W1, a1;

then xx in ((UAp R) . {yy}) ` by XBOOLE_0:def 5;

then xx in (UAp R) . (((UAp R) . {yy}) `) by a3, a1;

then xx in UAp (((UAp R) . {yy}) `) by ROUGHS_2:def 11;

then consider z being object such that

J1: ( z in Class ( the InternalRel of R,xx) & z in ((UAp R) . {yy}) ` ) by XBOOLE_0:3, ROUGHS_2:7;

reconsider zz = z as Element of R by J1;

J2: [xx,zz] in the InternalRel of R by J1, RELAT_1:169;

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

then not [z,y] in the InternalRel of R by a1;

hence ex z being object st

( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) by J2; :: thesis: verum

then R is positive_alliance ;

hence ex R being non empty finite positive_alliance RelStr st

( the carrier of R = A & U = UAp R ) by a1; :: thesis: verum