reconsider F = id (On U) as Ordinal-Sequence of U ;
take F ; :: thesis: F is normal
thus F is normal ; :: thesis: verum