let R1, R2 be Relation; :: thesis: ( ( for x, y being object holds
( [x,y] in R1 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) & ( for x, y being object holds
( [x,y] in R2 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) implies R1 = R2 )
assume that
A1: for x, y being object holds
( [x,y] in R1 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) and
A2: for x, y being object holds
( [x,y] in R2 iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ; :: thesis: R1 = R2
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )
thus ( [x,y] in R1 implies [x,y] in R2 ) :: thesis: ( not [x,y] in R2 or [x,y] in R1 )
proof
assume A3: [x,y] in R1 ; :: thesis: [x,y] in R2
then A4: ( x in field R & y in field R ) by A1;
ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) by A1, A3;
hence [x,y] in R2 by A2, A4; :: thesis: verum
end;
assume A5: [x,y] in R2 ; :: thesis: [x,y] in R1
then A6: ( x in field R & y in field R ) by A2;
ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) by A2, A5;
hence [x,y] in R1 by A1, A6; :: thesis: verum