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) `) = (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds
ex R being non empty finite 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) `) = (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ex R being non empty finite alliance RelStr st
( the carrier of R = A & U = UAp R ) )
assume A1:
( U . {} = {} & ( for X being Subset of A holds U . ((U . X) `) = (U . X) ` ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) )
; ex R being non empty finite alliance RelStr st
( the carrier of R = A & U = UAp R )
then
for X being Subset of A holds U . ((U . X) `) c= (U . X) `
;
then consider R being non empty finite negative_alliance RelStr such that
A2:
( the carrier of R = A & U = UAp R )
by Prop14, A1;
for X being Subset of A holds (U . X) ` c= U . ((U . X) `)
by A1;
then consider S being non empty finite positive_alliance RelStr such that
A3:
( the carrier of S = A & U = UAp S )
by Prop11, A1;
A4:
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #)
by A2, A3, Corr3A;
set RR = RelStr(# the carrier of R, the InternalRel of R #);
A5:
RelStr(# the carrier of R, the InternalRel of R #) is positive_alliance
by A4, PosReg;
RelStr(# the carrier of R, the InternalRel of R #) is negative_alliance
by NegReg;
then reconsider RR = RelStr(# the carrier of R, the InternalRel of R #) as non empty finite alliance RelStr by A5;
UAp RR = UAp R
by The5;
hence
ex R being non empty finite alliance RelStr st
( the carrier of R = A & U = UAp R )
by A2; verum