theorem YaoTh3: :: ROUGHS_3:14

for A being non empty finite set
for L, H being Function of (bool A),(bool A) st L = Flip H holds
( ( H . {} = {} & ( for X, Y being Subset of A holds H . (X \/ Y) = (H . X) \/ (H . Y) ) ) iff ex R being non empty finite RelStr st
( the carrier of R = A & LAp R = L & UAp R = H & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff x in H . {y} ) ) ) )