let X be non empty set ; :: thesis: for R being Relation of X
for x being Element of X
for y being set st R reduces x,y holds
y in X
let R be Relation of X; :: thesis: for x being Element of X
for y being set st R reduces x,y holds
y in X
let x be Element of X; :: thesis: for y being set st R reduces x,y holds
y in X
let y be set ; :: thesis: ( R reduces x,y implies y in X )
given p being RedSequence of R such that A1: ( p . 1 = x & p . (len p) = y ) ; :: according to REWRITE1:def 3 :: thesis: y in X
len p >= 0 + 1 by NAT_1:13;
then ( len p in dom p & p is FinSequence of X ) by A1, Th74, FINSEQ_3:27;
then ( y in rng p & rng p c= X ) by A1, FINSEQ_1:def 4, FUNCT_1:12;
hence y in X ; :: thesis: verum