now :: thesis: for b, c being Ordinal st b in c & c in dom (A | a) holds
(A | a) . c in (A | a) . b
let b, c be Ordinal; :: thesis: ( b in c & c in dom (A | a) implies (A | a) . c in (A | a) . b )
assume A1: ( b in c & c in dom (A | a) ) ; :: thesis: (A | a) . c in (A | a) . b
then A2: ( (A | a) . b = A . b & (A | a) . c = A . c ) by FUNCT_1:47, ORDINAL1:10;
c in dom A by A1, RELAT_1:57;
hence (A | a) . c in (A | a) . b by A1, A2, ORDINAL5:def 1; :: thesis: verum
end;
hence A | a is decreasing by ORDINAL5:def 1; :: thesis: verum