theorem Th24: :: HALLMAR1:24

for F being non empty finite set
for A being non-empty FinSequence of bool F
for i, j being Element of NAT
for B being Singlification of A,i
for C being Singlification of B,j st i in dom A & j in dom A & C . i <> {} & B . j <> {} holds
( C is Singlification of A,j & C is Singlification of A,i )