let n be Nat; :: thesis: for x being set holds
( x in the InternalRel of (Necklace n) iff ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) )
let x be set ; :: thesis: ( x in the InternalRel of (Necklace n) iff ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) )
thus ( x in the InternalRel of (Necklace n) implies ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) ) :: thesis: ( ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) implies x in the InternalRel of (Necklace n) )

proof

assume x in the InternalRel of (Necklace n) ; :: thesis: ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) )
then x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n } by Th17;
then ( x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or x in { [(i + 1),i] where i is Element of NAT : i + 1 < n } ) by XBOOLE_0:def 3;
then ( ex i being Element of NAT st
( x = [i,(i + 1)] & i + 1 < n ) or ex i being Element of NAT st
( x = [(i + 1),i] & i + 1 < n ) ) ;
hence ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) ; :: thesis: verum

end;

thus ( ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) implies x in the InternalRel of (Necklace n) ) :: thesis: verum

proof

given i being Element of NAT such that A1: ( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) ; :: thesis: x in the InternalRel of (Necklace n)

per cases ( ( i + 1 < n & x = [i,(i + 1)] ) or ( i + 1 < n & x = [(i + 1),i] ) ) by A1;

suppose ( i + 1 < n & x = [i,(i + 1)] ) ; :: thesis: x in the InternalRel of (Necklace n)

then x in { [j,(j + 1)] where j is Element of NAT : j + 1 < n } ;
then x in { [j,(j + 1)] where j is Element of NAT : j + 1 < n } \/ { [(j + 1),j] where j is Element of NAT : j + 1 < n } by XBOOLE_0:def 3;
hence x in the InternalRel of (Necklace n) by Th17; :: thesis: verum

end;

suppose ( i + 1 < n & x = [(i + 1),i] ) ; :: thesis: x in the InternalRel of (Necklace n)

then x in { [(j + 1),j] where j is Element of NAT : j + 1 < n } ;
then x in { [(j + 1),j] where j is Element of NAT : j + 1 < n } \/ { [j,(j + 1)] where j is Element of NAT : j + 1 < n } by XBOOLE_0:def 3;
hence x in the InternalRel of (Necklace n) by Th17; :: thesis: verum

end;

end;

end;