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 Element of 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 Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) ) )
assume A1: ( x in Y & 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 Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) )
then reconsider Y' = Y as non empty set ;
reconsider x' = x, y' = y as Element of Y' by A1;
reconsider R = union X as Relation of Y' by Th6;
R = R ~ by Th9;
then A2: R \/ (R ~ ) = R ;
A3: ( [x,y] in "\/" X iff R reduces x,y )

proof

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

proof

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

end;

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

proof

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

end;

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 Element of 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 Element of 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 Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) )
then consider f being FinSequence such that
A4: ( len f > 0 & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st i in dom f & i + 1 in dom f holds
[(f . i),(f . (i + 1))] in R ) ) by A3, REWRITE1:12;
take f ; :: thesis: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) )
0 + 1 <= len f by A4, NAT_1:13;
hence ( 1 <= len f & x = f . 1 & y = f . (len f) ) by A4; :: thesis: for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X
let i be Element of 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 A4; :: thesis: verum

end;

thus ( ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of 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 A5: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) ; :: thesis: [x,y] in "\/" X
0 + 1 <= len f by A5;
then A6: len f > 0 by NAT_1:13;

now

let i be Element of 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 A5; :: thesis: verum

end;

hence [x,y] in "\/" X by A3, A5, A6, REWRITE1:12; :: thesis: verum

end;