background image

6. INTERIOR FUNCOIDS

39

Proof.

g

v

f

h

⇔ ∀

X

A

:

h

g

i

X

v h

f

h

i

X

⇔ ∀

X

A

:

h

g

i

X

v h

f

i

h

h

i

X

⇔ ∀

X

A

:

h

g

i

X

v ¬h

f

i

¬h

h

i

X

⇔ ∀

X

A

:

h

g

i

X

h

f

i

¬h

h

i

X

⇔ ∀

X

A

:

f

1

h

g

i

X

 ¬h

h

i

X

⇔ ∀

X

A

:

f

1

h

g

i

X

v

h

h

i

X

⇔ ∀

X

A

:

f

1

g

X

v h

h

i

X

f

1

g

v

h

.

Remark

2223

.

The above theorem allows to get rid of interior funcoids (and

use only “regular” funcoids) in some formulas.