let f be Relation; :: thesis: for n, m being Nat holds (f | (n + m)) | n = f | n
let n, m be Nat; :: thesis: (f | (n + m)) | n = f | n
n /\ (n + m) = n ;
hence (f | (n + m)) | n = f | n by RELAT_1:71; :: thesis: verum