theorem Th29: :: ROUGHS_2:29

for A being non empty finite set
for U being Function of (bool A),(bool A) st U . {} = {} & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds
ex R being non empty finite RelStr st
( the carrier of R = A & U = UAp R )