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) `) = (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); :: thesis: ( 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) ) ) ; :: thesis: 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; :: thesis: verum

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); :: thesis: ( 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) ) ) ; :: thesis: 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; :: thesis: verum