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