let A be non empty finite set ; 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); ( 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) ) )
; 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
let x,
y be
object ;
( 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 )
;
( 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 )
;
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;
verum
end;
then
the InternalRel of R is_negative_alliance_in the carrier 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; verum