let x, y, Y be set ; :: thesis: for X being Subset of (EqRelLatt Y) st x in Y & y in Y holds
( [x,y] in "\/" X iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) )
let X be Subset of (EqRelLatt Y); :: thesis: ( x in Y & y in Y implies ( [x,y] in "\/" X iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) ) )
assume that
A1: x in Y and
A2: y in Y ; :: thesis: ( [x,y] in "\/" X iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) )
reconsider Y9 = Y as non empty set by A1;
reconsider x9 = x, y9 = y as Element of Y9 by A1, A2;
reconsider R = union X as Relation of Y9 by Th6;
R = R ~ by Th9;
then A3: R \/ (R ~) = R ;
A4: ( [x,y] in "\/" X implies R reduces x,y )

proof

assume [x,y] in "\/" X ; :: thesis: R reduces x,y
then [x9,y9] in EqCl R by Th8;
then x,y are_convertible_wrt R by MSUALG_6:41;
hence R reduces x,y by A3, REWRITE1:def 4; :: thesis: verum

end;

thus ( [x,y] in "\/" X implies ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) ) :: thesis: ( ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) implies [x,y] in "\/" X )

proof

assume [x,y] in "\/" X ; :: thesis: ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) )
then consider f being FinSequence such that
A5: len f > 0 and
A6: ( x = f . 1 & y = f . (len f) ) and
A7: for i being Nat st i in dom f & i + 1 in dom f holds
[(f . i),(f . (i + 1))] in R by A4, REWRITE1:11;
take f ; :: thesis: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) )
0 + 1 <= len f by A5, NAT_1:13;
hence ( 1 <= len f & x = f . 1 & y = f . (len f) ) by A6; :: thesis: for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X
let i be Nat; :: thesis: ( 1 <= i & i < len f implies [(f . i),(f . (i + 1))] in union X )
assume ( 1 <= i & i < len f ) ; :: thesis: [(f . i),(f . (i + 1))] in union X
then ( i in dom f & i + 1 in dom f ) by Th1;
hence [(f . i),(f . (i + 1))] in union X by A7; :: thesis: verum

end;

A8: ( R reduces x,y implies [x,y] in "\/" X )

proof

assume R reduces x,y ; :: thesis: [x,y] in "\/" X
then x,y are_convertible_wrt R by REWRITE1:25;
then [x9,y9] in EqCl R by MSUALG_6:41;
hence [x,y] in "\/" X by Th8; :: thesis: verum

end;

thus ( ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) implies [x,y] in "\/" X ) :: thesis: verum

proof

given f being FinSequence such that A9: 1 <= len f and
A10: ( x = f . 1 & y = f . (len f) ) and
A11: for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ; :: thesis: [x,y] in "\/" X

A12: now :: thesis: for i being Nat st i in dom f & i + 1 in dom f holds
[(f . i),(f . (i + 1))] in union X

let i be Nat; :: thesis: ( i in dom f & i + 1 in dom f implies [(f . i),(f . (i + 1))] in union X )
assume ( i in dom f & i + 1 in dom f ) ; :: thesis: [(f . i),(f . (i + 1))] in union X
then ( 1 <= i & i < len f ) by Th1;
hence [(f . i),(f . (i + 1))] in union X by A11; :: thesis: verum

end;

0 + 1 <= len f by A9;
then len f > 0 by NAT_1:13;
hence [x,y] in "\/" X by A8, A10, A12, REWRITE1:11; :: thesis: verum

end;