let e be empty set ; :: thesis: ( e is decreasing & e is increasing )
thus e is decreasing :: thesis: e is increasing

proof

let a be ordinal number ; :: according to ORDINAL5:def 1 :: thesis: for b being ordinal number st a in b & b in dom e holds
e . b in e . a
thus for b being ordinal number st a in b & b in dom e holds
e . b in e . a ; :: thesis: verum

end;

let a be ordinal number ; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not a in b₁ or not b₁ in proj1 e or e . a in e . b₁ )
thus for b₁ being set holds
( not a in b₁ or not b₁ in proj1 e or e . a in e . b₁ ) ; :: thesis: verum