theorem Th32: :: ROUGHS_2:32

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