let A be non empty finite set ; :: thesis: for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds (L . X) ` c= L . ((L . X) `) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds
ex R being non empty finite negative_alliance RelStr st
( the carrier of R = A & L = LAp R )
let L be Function of (bool A),(bool A); :: thesis: ( L . A = A & ( for X being Subset of A holds (L . X) ` c= L . ((L . X) `) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) implies ex R being non empty finite negative_alliance RelStr st
( the carrier of R = A & L = LAp R ) )
assume that
A1: L . A = A and
A3: for X being Subset of A holds (L . X) ` c= L . ((L . X) `) and
A4: for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ; :: thesis: ex R being non empty finite negative_alliance RelStr st
( the carrier of R = A & L = LAp R )
set U = Flip L;
C1: (Flip L) . {} = {} by A1, ROUGHS_2:19;
C2: for X being Subset of A holds (Flip L) . (((Flip L) . X) `) c= ((Flip L) . X) ` by A3, Conv2;
for X, Y being Subset of A holds (Flip L) . (X \/ Y) = ((Flip L) . X) \/ ((Flip L) . Y) by A4, ROUGHS_2:22;
then consider R being non empty finite negative_alliance RelStr such that
A2: ( the carrier of R = A & Flip L = UAp R ) by Prop14, C1, C2;
Flip (Flip L) = LAp R by A2, ROUGHS_2:27;
then L = LAp R by ROUGHS_2:23;
hence ex R being non empty finite negative_alliance RelStr st
( the carrier of R = A & L = LAp R ) by A2; :: thesis: verum