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) ` = 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 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) ` = 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 alliance RelStr st

( the carrier of R = A & L = LAp R ) )

assume A0: ( L . A = A & ( for X being Subset of A holds (L . X) ` = L . ((L . X) `) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) ) ; :: thesis: ex R being non empty finite alliance RelStr st

( the carrier of R = A & L = LAp R )

set U = Flip L;

A2: (Flip L) . {} = {} by A0, ROUGHS_2:19;

A3: for X being Subset of A holds (Flip L) . (((Flip L) . X) `) = ((Flip L) . X) `

then consider R being non empty finite alliance RelStr such that

A1: ( the carrier of R = A & Flip L = UAp R ) by A2, A3, Th2H;

Flip (Flip L) = L by ROUGHS_2:23;

then L = LAp R by A1, ROUGHS_2:27;

hence ex R being non empty finite alliance RelStr st

( the carrier of R = A & L = LAp R ) by A1; :: thesis: verum

ex R being non empty finite 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) ` = 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 alliance RelStr st

( the carrier of R = A & L = LAp R ) )

assume A0: ( L . A = A & ( for X being Subset of A holds (L . X) ` = L . ((L . X) `) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) ) ; :: thesis: ex R being non empty finite alliance RelStr st

( the carrier of R = A & L = LAp R )

set U = Flip L;

A2: (Flip L) . {} = {} by A0, ROUGHS_2:19;

A3: for X being Subset of A holds (Flip L) . (((Flip L) . X) `) = ((Flip L) . X) `

proof

for X, Y being Subset of A holds (Flip L) . (X \/ Y) = ((Flip L) . X) \/ ((Flip L) . Y)
by A0, ROUGHS_2:22;
let X be Subset of A; :: thesis: (Flip L) . (((Flip L) . X) `) = ((Flip L) . X) `

for X being Subset of A holds (L . X) ` c= L . ((L . X) `) by A0;

then Z1: (Flip L) . (((Flip L) . X) `) c= ((Flip L) . X) ` by Conv2;

Z2: L = Flip (Flip L) by ROUGHS_2:23;

for X being Subset of A holds L . ((L . X) `) c= (L . X) ` by A0;

then ((Flip L) . X) ` c= (Flip L) . (((Flip L) . X) `) by Conv3, Z2;

hence (Flip L) . (((Flip L) . X) `) = ((Flip L) . X) ` by Z1, XBOOLE_0:def 10; :: thesis: verum

end;for X being Subset of A holds (L . X) ` c= L . ((L . X) `) by A0;

then Z1: (Flip L) . (((Flip L) . X) `) c= ((Flip L) . X) ` by Conv2;

Z2: L = Flip (Flip L) by ROUGHS_2:23;

for X being Subset of A holds L . ((L . X) `) c= (L . X) ` by A0;

then ((Flip L) . X) ` c= (Flip L) . (((Flip L) . X) `) by Conv3, Z2;

hence (Flip L) . (((Flip L) . X) `) = ((Flip L) . X) ` by Z1, XBOOLE_0:def 10; :: thesis: verum

then consider R being non empty finite alliance RelStr such that

A1: ( the carrier of R = A & Flip L = UAp R ) by A2, A3, Th2H;

Flip (Flip L) = L by ROUGHS_2:23;

then L = LAp R by A1, ROUGHS_2:27;

hence ex R being non empty finite alliance RelStr st

( the carrier of R = A & L = LAp R ) by A1; :: thesis: verum