environ
vocabularies HIDDEN, ORDINAL6, EXCHSORT, ZFMISC_1, XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, ORDINAL2, ORDINAL4, FINSET_1, RELAT_2, FUNCT_4, FINSEQ_1, AOFA_000, FUNCT_3, VALUED_0, WELLFND1, CARD_1, TARSKI, FUNCT_2, PARTFUN1, FUNCT_7, REARRAN1, ORDINAL3, NAT_1, SUBSET_1, XXREAL_0, ARYTM_3, AFINSQ_1, REWRITE1, NUMBERS, MSUALG_1, MEMBERED, STRUCT_0, ORDERS_2, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, FINSEQ_1, BINOP_1, FUNCT_4, FUNCT_7, ORDINAL1, NUMBERS, MEMBERED, VALUED_0, CARD_1, XCMPLX_0, ORDINAL2, ORDINAL3, ORDINAL4, AFINSQ_1, STRUCT_0, ORDERS_2, WAYBEL_0, XXREAL_0, XREAL_0, NAT_1, AOFA_000, ORDINAL5, FUNCT_3, ORDINAL6;
definitions TARSKI, XBOOLE_0, RELAT_1, RELAT_2, PARTFUN1, FUNCT_2, ORDINAL1, WELLORD2, FUNCT_1, VALUED_0, ORDINAL5, ORDINAL6;
theorems TARSKI, CARD_1, ZFMISC_1, ORDINAL1, ORDINAL2, RELAT_1, RELSET_1, MEMBERED, FINSET_1, CARD_2, TREES_1, GRFUNC_1, FUNCT_2, XBOOLE_1, FINSEQ_3, NAT_1, XBOOLE_0, ORDINAL3, XXREAL_0, SETFAM_1, ORDINAL4, FUNCT_1, FUNCT_7, SUBSET_1, FUNCT_3, FUNCT_4, FUNCT_5, AFINSQ_1, PARTFUN1, ORDERS_2, YELLOW_0, WAYBEL_0, ORDINAL6, XTUPLE_0;
schemes NAT_1, ORDINAL2, RECDEF_1;
registrations MEMBERED, SUBSET_1, RELSET_1, XXREAL_0, XBOOLE_0, FINSET_1, RELAT_1, FUNCT_1, ORDINAL1, VALUED_0, ORDINAL5, AFINSQ_1, CARD_1, FUNCT_2, FUNCT_7, FUNCTOR1, STRUCT_0, WAYBEL_0, ORDINAL6, XCMPLX_0;
constructors HIDDEN, MEMBERED, VALUED_0, CATALAN2, ORDINAL3, INT_1, FUNCT_7, ORDINAL5, WELLORD2, RELAT_2, FACIRC_1, BINOP_1, WAYBEL_0, RELSET_1, ORDINAL6, XTUPLE_0;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL;
equalities ORDINAL1, ORDINAL2, BINOP_1, CARD_1;
expansions TARSKI, XBOOLE_0, ORDINAL1, WELLORD2, FUNCT_1, VALUED_0;
defpred S1[ set , set , set , set ] means ( $3 <> $1 & $3 <> $2 & $4 <> $1 & $4 <> $2 );
defpred S2[ set , set , set , set ] means ( $3 in $1 & $4 = $1 );
defpred S3[ set , set , set , set ] means ( $3 in $1 & $4 = $2 );
defpred S4[ set , set , set , set ] means ( $3 = $1 & $4 in $2 );
defpred S5[ set , set , set , set ] means ( $3 = $1 & $4 = $2 );
defpred S6[ set , set , set , set ] means ( $3 = $1 & $2 in $4 );
defpred S7[ set , set , set , set ] means ( $1 in $3 & $4 = $2 );
defpred S8[ set , set , set , set ] means ( $3 = $2 & $2 in $4 );
theorem Th2:
for
a,
b,
c,
d being
Ordinal st
a in b &
c in d & not (
c <> a &
c <> b &
d <> a &
d <> b ) & not (
c in a &
d = a ) & not (
c in a &
d = b ) & not (
c = a &
d in b ) & not (
c = a &
d = b ) & not (
c = a &
b in d ) & not (
a in c &
d = b ) holds
(
c = b &
b in d )
::
deftheorem defines
incl EXCHSORT:def 13 :
for O being non empty connected Poset
for R being array of O
for x, y being set holds (R,x,y) incl = [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] +* (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]));
theorem Th62:
for
O being non
empty connected Poset for
T being non
empty array of
O for
p,
q,
r being
Element of
dom T st
p c= r &
r c= q holds
(
((T,p,q) incl) . (
p,
r)
= [p,r] &
((T,p,q) incl) . (
r,
q)
= [r,q] )
theorem Th64:
for
f being
Function for
O being non
empty connected Poset for
T being non
empty array of
O for
p,
q,
r being
Element of
dom T st
r in p &
f = Swap (
(id (dom T)),
p,
q) holds
(
((T,p,q) incl) . (
r,
q)
= [(f . r),(f . q)] &
((T,p,q) incl) . (
r,
p)
= [(f . r),(f . p)] )
theorem Th65:
for
f being
Function for
O being non
empty connected Poset for
T being non
empty array of
O for
p,
q,
r being
Element of
dom T st
q in r &
f = Swap (
(id (dom T)),
p,
q) holds
(
((T,p,q) incl) . (
p,
r)
= [(f . p),(f . r)] &
((T,p,q) incl) . (
q,
r)
= [(f . q),(f . r)] )
theorem Th68:
for
O being non
empty connected Poset for
T being non
empty array of
O for
p,
q,
r being
Element of
dom T st
r in p &
p in q holds
(
((T,p,q) incl) . (
r,
p)
= [r,q] &
((T,p,q) incl) . (
r,
q)
= [r,p] )
theorem Th69:
for
O being non
empty connected Poset for
T being non
empty array of
O for
p,
q,
s being
Element of
dom T st
p in s &
s in q holds
(
((T,p,q) incl) . (
p,
s)
= [p,s] &
((T,p,q) incl) . (
s,
q)
= [s,q] )
theorem Th70:
for
O being non
empty connected Poset for
T being non
empty array of
O for
p,
q,
s being
Element of
dom T st
p in q &
q in s holds
(
((T,p,q) incl) . (
p,
s)
= [q,s] &
((T,p,q) incl) . (
q,
s)
= [p,s] )
Lm1:
for f being Function
for O being non empty connected Poset
for T being non empty array of O
for p, q being Element of dom T st p in q & f = (T,p,q) incl holds
for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )