10 hours later…
2:22 PM
2:51 PM
3 hours later…
5:47 PM
∀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 )
« first day (3932 days earlier) ← previous day next day → last day (1012 days later) »