let R, Q be Relation; ( R c= Q implies for a, b being object st R reduces a,b holds
Q reduces a,b )
assume A1:
R c= Q
; for a, b being object st R reduces a,b holds
Q reduces a,b
let a, b be object ; ( R reduces a,b implies Q reduces a,b )
given p being RedSequence of R such that A2:
( p . 1 = a & p . (len p) = b )
; REWRITE1:def 3 Q reduces a,b
p is RedSequence of Q
by A1, Th10;
hence
ex p being RedSequence of Q st
( p . 1 = a & p . (len p) = b )
by A2; REWRITE1:def 3 verum