begin
theorem
canceled;
theorem
theorem
for
x1,
x2,
x3,
y1,
y2,
y3 being
set holds
[:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}
theorem Th4:
for
x being
set for
n being
Nat st
x in n holds
x is
Nat
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem
theorem Th10:
theorem Th11:
for
a,
b,
c,
d being
set holds
not ( (
a = b implies
c = d ) & (
c = d implies
a = b ) & not
(a,b --> c,d) " = c,
d --> a,
b )
theorem
for
i,
j,
n being
Nat st
i < j &
j in n holds
i in n
begin
:: deftheorem NECKLACE:def 1 :
canceled;
:: deftheorem Def2 defines embeds NECKLACE:def 2 :
theorem Th13:
:: deftheorem Def3 defines is_equimorphic_to NECKLACE:def 3 :
theorem
:: deftheorem Def4 defines symmetric NECKLACE:def 4 :
:: deftheorem Def5 defines asymmetric NECKLACE:def 5 :
theorem
:: deftheorem defines irreflexive NECKLACE:def 6 :
:: deftheorem Def7 defines -SuccRelStr NECKLACE:def 7 :
theorem
theorem Th17:
:: deftheorem Def8 defines SymRelStr NECKLACE:def 8 :
Lm1:
for S, R being non empty RelStr st S,R are_isomorphic holds
card the InternalRel of S = card the InternalRel of R
:: deftheorem Def9 defines ComplRelStr NECKLACE:def 9 :
theorem Th18:
begin
:: deftheorem defines Necklace NECKLACE:def 10 :
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem
theorem