Proofgold Proposition

∀ x0 x1 : ι → ο . wceq (cwlim x0 x1) (crab (λ x2 . wa (wne (cv x2) (cinf x0 x0 x1)) (wceq (cv x2) (csup (cpred x0 x1 (cv x2)) x0 x1))) (λ x2 . x0))

type
prop

theory
SetMM

name
df_wlim

proof
PUcix..

Megalodon
-

proofgold address
TMEp8..

creator
36378 PrCmT../99a84..

owner
36378 PrCmT../99a84..

term root
b3323..