let n be Nat; :: thesis:
set S = n -SuccRelStr ;
the InternalRel of () is_asymmetric_in field the InternalRel of ()
proof
let x, y be object ; :: according to RELAT_2:def 5 :: thesis: ( not x in field the InternalRel of () or not y in field the InternalRel of () or not [x,y] in the InternalRel of () or not [y,x] in the InternalRel of () )
assume that
x in field the InternalRel of () and
y in field the InternalRel of () and
A1: [x,y] in the InternalRel of () ; :: thesis: not [y,x] in the InternalRel of ()
A2: [x,y] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by ;
assume [y,x] in the InternalRel of () ; :: thesis: contradiction
then [y,x] in { [i9,(i9 + 1)] where i9 is Element of NAT : i9 + 1 < n } by Def6;
then consider j being Element of NAT such that
A3: [y,x] = [j,(j + 1)] and
j + 1 < n ;
A4: ( y = j & x = j + 1 ) by ;
consider i being Element of NAT such that
A5: [x,y] = [i,(i + 1)] and
i + 1 < n by A2;
( x = i & y = i + 1 ) by ;
hence contradiction by A4; :: thesis: verum
end;
hence the InternalRel of () is asymmetric ; :: according to NECKLACE:def 4 :: thesis: verum