This paper proves that Zermelo-Fraenkel set theory (ZF) is consistent within the type theory of Lean, using only excluded middle and no additional axioms like choice or propositional extensionality. The proof employs large elimination of the accessibility predicate to construct ordinals and validate the Replacement axiom, showing that ZF has a model in this type-theoretic framework.