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 . ((U . X) `) c= (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite negative_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 . ((U . X) `) c= (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ex R being non empty finite negative_alliance RelStr st

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

assume a0: ( U . {} = {} & ( for X being Subset of A holds U . ((U . X) `) c= (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) ) ; :: thesis: ex R being non empty finite negative_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 & 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 ) holds

not [x,y] in the InternalRel of R

then R is negative_alliance ;

hence ex R being non empty finite negative_alliance RelStr st

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

ex R being non empty finite negative_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 . ((U . X) `) c= (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ex R being non empty finite negative_alliance RelStr st

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

assume a0: ( U . {} = {} & ( for X being Subset of A holds U . ((U . X) `) c= (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) ) ; :: thesis: ex R being non empty finite negative_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 & 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 ) holds

not [x,y] in the InternalRel of R

proof

then
the InternalRel of R is_negative_alliance_in the carrier of R
;
let x, y be object ; :: thesis: ( x in the carrier of R & y in the carrier of R & 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 ) implies not [x,y] in the InternalRel of R )

assume ( x in the carrier of R & y in the carrier of R ) ; :: thesis: ( for z being object holds

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

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

given z being object such that A1: ( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) ; :: thesis: not [x,y] in the InternalRel of R

reconsider zz = z as Element of R by A1;

not zz in (UAp R) . {yy} by A1, a1;

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

B1: zz in Class ( the InternalRel of R,xx) by RELAT_1:169, A1;

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

Class ( the InternalRel of R,xx) meets ((UAp R) . {yy}) ` by B1, XBOOLE_0:3, B0;

then xx in { x where x is Element of R : Class ( the InternalRel of R,x) meets ((UAp R) . {yy}) ` } ;

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

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

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

hence not [x,y] in the InternalRel of R by a1; :: thesis: verum

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

assume ( x in the carrier of R & y in the carrier of R ) ; :: thesis: ( for z being object holds

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

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

given z being object such that A1: ( z in the carrier of R & [x,z] in the InternalRel of R & not [z,y] in the InternalRel of R ) ; :: thesis: not [x,y] in the InternalRel of R

reconsider zz = z as Element of R by A1;

not zz in (UAp R) . {yy} by A1, a1;

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

B1: zz in Class ( the InternalRel of R,xx) by RELAT_1:169, A1;

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

Class ( the InternalRel of R,xx) meets ((UAp R) . {yy}) ` by B1, XBOOLE_0:3, B0;

then xx in { x where x is Element of R : Class ( the InternalRel of R,x) meets ((UAp R) . {yy}) ` } ;

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

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

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

hence not [x,y] in the InternalRel of R by a1; :: thesis: verum

then R is negative_alliance ;

hence ex R being non empty finite negative_alliance RelStr st

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