let A be non empty finite set ; 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); ( 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) ) )
; 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) `
for X, Y being Subset of A holds (Flip L) . (X \/ Y) = ((Flip L) . X) \/ ((Flip L) . Y)
by A0, ROUGHS_2:22;
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; verum