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) )

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

( 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

thus
( ex i being Element of NAT st
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;( 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

( 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)

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

end;

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;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

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;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