∀S∈obj ( S∈set ∧ ∃X∈set ( X∈S ) ⇔ S∈set ∧ S ∈ nset ) [Lemma]
Define nset to be the type { S : S∈set ∧ ∃A∈set ( A∈S ) }
Given S ∈ obj:
If S ∈ set ∧ ∃ X ∈ set ( X ∈ S ):
∃ X ∈ set ( X ∈ S )
Let X' ∈ set such that X' ∈ S
X' ∈ set ∧ X' ∈ S
∃A∈set ( A∈S ) [A is unused]
S∈set ∧ ∃A∈set ( A∈S )
S ∈ { S : S∈set ∧ ∃A∈set ( A∈S ) }
S ∈ nset
S∈set ∧ S ∈ nset
If S∈set ∧ S ∈ nset:
S ∈ nset
S ∈ { S : S∈set ∧ ∃A∈set ( A∈S ) }
S ∈ set ∧ ∃ A ∈ set ( A ∈ S )
There is no way I can find to get to this room I circled and have never seen it before. I am on the corpse floor 1.
