let R, Q be Relation; :: thesis: ( R c= Q implies for a, b being set st R reduces a,b holds
Q reduces a,b )
assume A1: R c= Q ; :: thesis: for a, b being set st R reduces a,b holds
Q reduces a,b
let a, b be set ; :: thesis: ( 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 ) ; :: according to REWRITE1:def 3 :: thesis: Q reduces a,b
p is RedSequence of Q by A1, Th11;
hence ex p being RedSequence of Q st
( p . 1 = a & p . (len p) = b ) by A2; :: according to REWRITE1:def 3 :: thesis: verum