let e be empty set ; :: thesis: ( e is decreasing & e is increasing )
thus e is decreasing ; :: thesis: e is increasing
let a be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not a in b₁ or not b₁ in dom e or e . a in e . b₁ )
thus for b₁ being set holds
( not a in b₁ or not b₁ in dom e or e . a in e . b₁ ) ; :: thesis: verum