:: CHAIN_1 semantic presentation

theorem Th1: :: CHAIN_1:1
for b1, b2 being real number st b1 < b2 holds
ex b3 being Real st
( b1 < b3 & b3 < b2 )
proof end;

theorem Th2: :: CHAIN_1:2
for b1, b2 being real number ex b3 being Real st
( b1 < b3 & b2 < b3 )
proof end;

scheme :: CHAIN_1:sch 1
s1{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ], F3( set , set ) -> Element of F1() } :
{ F3(b1,b2) where B is Element of F2(), B is Element of F2() : P1[b1,b2] } c= F1()
proof end;

definition
let c1 be set ;
let c2 be Subset of c1;
redefine func bool as bool c2 -> Subset-Family of a1;
coherence
bool c2 is Subset-Family of c1 by ZFMISC_1:79;
end;

definition
let c1 be real Nat;
redefine attr a1 is empty means :: CHAIN_1:def 1
not a1 > 0;
compatibility
( c1 is zero iff not c1 > 0 ) ;
end;

:: deftheorem Def1 defines zero CHAIN_1:def 1 :
for b1 being real Nat holds
( b1 is zero iff not b1 > 0 );

definition
let c1 be Nat;
redefine attr a1 is empty means :Def2: :: CHAIN_1:def 2
not a1 >= 1;
compatibility
( c1 is zero iff not c1 >= 1 )
proof end;
end;

:: deftheorem Def2 defines zero CHAIN_1:def 2 :
for b1 being Nat holds
( b1 is zero iff not b1 >= 1 );

registration
cluster non zero Element of NAT ;
existence
not for b1 being Nat holds b1 is zero
proof end;
end;

registration
let c1 be non zero Nat;
cluster Seg a1 -> non empty ;
coherence
not Seg c1 is zero by FINSEQ_1:5;
end;

definition
let c1 be set ;
redefine attr a1 is trivial means :Def3: :: CHAIN_1:def 3
for b1, b2 being set st b1 in a1 & b2 in a1 holds
b1 = b2;
compatibility
( c1 is trivial iff for b1, b2 being set st b1 in c1 & b2 in c1 holds
b1 = b2 )
proof end;
end;

:: deftheorem Def3 defines trivial CHAIN_1:def 3 :
for b1 being set holds
( b1 is trivial iff for b2, b3 being set st b2 in b1 & b3 in b1 holds
b2 = b3 );

theorem Th3: :: CHAIN_1:3
canceled;

theorem Th4: :: CHAIN_1:4
for b1, b2 being set holds
( {b1,b2} is trivial iff b1 = b2 )
proof end;

registration
cluster finite non trivial set ;
existence
ex b1 being set st
( not b1 is trivial & b1 is finite )
proof end;
end;

registration
let c1 be non trivial set ;
let c2 be set ;
cluster a1 \/ a2 -> non trivial ;
coherence
not c1 \/ c2 is trivial
proof end;
cluster a2 \/ a1 -> non trivial ;
coherence
not c2 \/ c1 is trivial ;
end;

registration
cluster REAL -> non trivial ;
coherence
not REAL is trivial
proof end;
end;

registration
let c1 be non trivial set ;
cluster finite non trivial Element of bool a1;
existence
ex b1 being Subset of c1 st
( not b1 is trivial & b1 is finite )
proof end;
end;

theorem Th5: :: CHAIN_1:5
for b1, b2 being set st b1 is trivial & not b1 \/ {b2} is trivial holds
ex b3 being set st b1 = {b3}
proof end;

scheme :: CHAIN_1:sch 2
s2{ F1() -> non empty set , F2() -> non empty finite Subset of F1(), P1[ set ] } :
P1[F2()]
provided
E7: for b1 being Element of F1() st b1 in F2() holds
P1[{b1}] and
E8: for b1 being Element of F1()
for b2 being non empty finite Subset of F1() st b1 in F2() & b2 c= F2() & not b1 in b2 & P1[b2] holds
P1[b2 \/ {b1}]
proof end;

scheme :: CHAIN_1:sch 3
s3{ F1() -> non trivial set , F2() -> finite non trivial Subset of F1(), P1[ set ] } :
P1[F2()]
provided
E7: for b1, b2 being Element of F1() st b1 in F2() & b2 in F2() & b1 <> b2 holds
P1[{b1,b2}] and
E8: for b1 being Element of F1()
for b2 being finite non trivial Subset of F1() st b1 in F2() & b2 c= F2() & not b1 in b2 & P1[b2] holds
P1[b2 \/ {b1}]
proof end;

theorem Th6: :: CHAIN_1:6
for b1 being set holds
( Card b1 = 2 iff ex b2, b3 being set st
( b2 in b1 & b3 in b1 & b2 <> b3 & ( for b4 being set holds
( not b4 in b1 or b4 = b2 or b4 = b3 ) ) ) )
proof end;

theorem Th7: :: CHAIN_1:7
for b1, b2 being Nat holds
( ( b1 is even iff b2 is even ) iff b1 + b2 is even )
proof end;

theorem Th8: :: CHAIN_1:8
for b1, b2 being finite set st b1 misses b2 holds
( ( card b1 is even iff card b2 is even ) iff card (b1 \/ b2) is even )
proof end;

theorem Th9: :: CHAIN_1:9
for b1, b2 being finite set holds
( ( card b1 is even iff card b2 is even ) iff card (b1 \+\ b2) is even )
proof end;

definition
let c1 be Nat;
redefine func REAL c1 -> FinSequenceSet of REAL means :Def4: :: CHAIN_1:def 4
for b1 being set holds
( b1 in a2 iff b1 is Function of Seg a1, REAL );
compatibility
for b1 being FinSequenceSet of REAL holds
( b1 = REAL c1 iff for b2 being set holds
( b2 in b1 iff b2 is Function of Seg c1, REAL ) )
proof end;
end;

:: deftheorem Def4 defines REAL CHAIN_1:def 4 :
for b1 being Nat
for b2 being FinSequenceSet of REAL holds
( b2 = REAL b1 iff for b3 being set holds
( b3 in b2 iff b3 is Function of Seg b1, REAL ) );

definition
let c1 be non zero Nat;
let c2 be Element of REAL c1;
let c3 be Element of Seg c1;
redefine func . as c2 . c3 -> Real;
coherence
c2 . c3 is Real
proof end;
end;

definition
let c1 be non zero Nat;
mode Grating of c1 -> Function of Seg a1, bool REAL means :Def5: :: CHAIN_1:def 5
for b1 being Element of Seg a1 holds
( not a2 . b1 is trivial & a2 . b1 is finite );
existence
ex b1 being Function of Seg c1, bool REAL st
for b2 being Element of Seg c1 holds
( not b1 . b2 is trivial & b1 . b2 is finite )
proof end;
end;

:: deftheorem Def5 defines Grating CHAIN_1:def 5 :
for b1 being non zero Nat
for b2 being Function of Seg b1, bool REAL holds
( b2 is Grating of b1 iff for b3 being Element of Seg b1 holds
( not b2 . b3 is trivial & b2 . b3 is finite ) );

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Element of Seg c1;
redefine func . as c2 . c3 -> finite non trivial Subset of REAL ;
coherence
c2 . c3 is finite non trivial Subset of REAL by Def5;
end;

theorem Th10: :: CHAIN_1:10
for b1 being non zero Nat
for b2 being Element of REAL b1
for b3 being Grating of b1 holds
( b2 in product b3 iff for b4 being Element of Seg b1 holds b2 . b4 in b3 . b4 )
proof end;

theorem Th11: :: CHAIN_1:11
for b1 being non zero Nat
for b2 being Grating of b1 holds product b2 is finite
proof end;

theorem Th12: :: CHAIN_1:12
for b1 being non empty finite Subset of REAL ex b2 being Real st
( b2 in b1 & ( for b3 being Real st b3 in b1 holds
b2 >= b3 ) )
proof end;

theorem Th13: :: CHAIN_1:13
for b1 being non empty finite Subset of REAL ex b2 being Real st
( b2 in b1 & ( for b3 being Real st b3 in b1 holds
b2 <= b3 ) )
proof end;

theorem Th14: :: CHAIN_1:14
for b1 being finite non trivial Subset of REAL ex b2, b3 being Real st
( b2 in b1 & b3 in b1 & b2 < b3 & ( for b4 being Real st b4 in b1 & b2 < b4 holds
not b4 < b3 ) )
proof end;

theorem Th15: :: CHAIN_1:15
for b1 being non empty finite Subset of REAL ex b2 being Real st
( b2 in b1 & ( for b3 being Real st b3 in b1 holds
b2 >= b3 ) ) by Th12;

theorem Th16: :: CHAIN_1:16
for b1 being finite non trivial Subset of REAL ex b2, b3 being Real st
( b2 in b1 & b3 in b1 & b3 < b2 & ( for b4 being Real st b4 in b1 holds
( not b4 < b3 & not b2 < b4 ) ) )
proof end;

definition
let c1 be finite non trivial Subset of REAL ;
mode Gap of c1 -> Element of [:REAL ,REAL :] means :Def6: :: CHAIN_1:def 6
ex b1, b2 being Real st
( a2 = [b1,b2] & b1 in a1 & b2 in a1 & ( ( b1 < b2 & ( for b3 being Real st b3 in a1 & b1 < b3 holds
not b3 < b2 ) ) or ( b2 < b1 & ( for b3 being Real st b3 in a1 holds
( not b1 < b3 & not b3 < b2 ) ) ) ) );
existence
ex b1 being Element of [:REAL ,REAL :]ex b2, b3 being Real st
( b1 = [b2,b3] & b2 in c1 & b3 in c1 & ( ( b2 < b3 & ( for b4 being Real st b4 in c1 & b2 < b4 holds
not b4 < b3 ) ) or ( b3 < b2 & ( for b4 being Real st b4 in c1 holds
( not b2 < b4 & not b4 < b3 ) ) ) ) )
proof end;
end;

:: deftheorem Def6 defines Gap CHAIN_1:def 6 :
for b1 being finite non trivial Subset of REAL
for b2 being Element of [:REAL ,REAL :] holds
( b2 is Gap of b1 iff ex b3, b4 being Real st
( b2 = [b3,b4] & b3 in b1 & b4 in b1 & ( ( b3 < b4 & ( for b5 being Real st b5 in b1 & b3 < b5 holds
not b5 < b4 ) ) or ( b4 < b3 & ( for b5 being Real st b5 in b1 holds
( not b3 < b5 & not b5 < b4 ) ) ) ) ) );

theorem Th17: :: CHAIN_1:17
for b1 being finite non trivial Subset of REAL
for b2, b3 being Real holds
( [b2,b3] is Gap of b1 iff ( b2 in b1 & b3 in b1 & ( ( b2 < b3 & ( for b4 being Real st b4 in b1 & b2 < b4 holds
not b4 < b3 ) ) or ( b3 < b2 & ( for b4 being Real st b4 in b1 holds
( not b2 < b4 & not b4 < b3 ) ) ) ) ) )
proof end;

theorem Th18: :: CHAIN_1:18
for b1 being finite non trivial Subset of REAL
for b2, b3, b4, b5 being Real st b1 = {b2,b3} holds
( [b4,b5] is Gap of b1 iff ( ( b4 = b2 & b5 = b3 ) or ( b4 = b3 & b5 = b2 ) ) )
proof end;

deffunc H1( set ) -> set = a1;

theorem Th19: :: CHAIN_1:19
for b1 being finite non trivial Subset of REAL
for b2 being Real st b2 in b1 holds
ex b3 being Real st [b2,b3] is Gap of b1
proof end;

theorem Th20: :: CHAIN_1:20
for b1 being finite non trivial Subset of REAL
for b2 being Real st b2 in b1 holds
ex b3 being Real st [b3,b2] is Gap of b1
proof end;

theorem Th21: :: CHAIN_1:21
for b1 being finite non trivial Subset of REAL
for b2, b3, b4 being Real st [b2,b3] is Gap of b1 & [b2,b4] is Gap of b1 holds
b3 = b4
proof end;

theorem Th22: :: CHAIN_1:22
for b1 being finite non trivial Subset of REAL
for b2, b3, b4 being Real st [b2,b3] is Gap of b1 & [b4,b3] is Gap of b1 holds
b2 = b4
proof end;

theorem Th23: :: CHAIN_1:23
for b1 being finite non trivial Subset of REAL
for b2, b3, b4, b5 being Real st b2 < b3 & [b3,b2] is Gap of b1 & b4 < b5 & [b5,b4] is Gap of b1 holds
( b3 = b5 & b2 = b4 )
proof end;

definition
let c1 be non zero Nat;
let c2, c3 be Element of REAL c1;
func cell c2,c3 -> non empty Subset of (REAL a1) equals :: CHAIN_1:def 7
{ b1 where B is Element of REAL a1 : ( for b1 being Element of Seg a1 holds
( a2 . b2 <= b1 . b2 & b1 . b2 <= a3 . b2 ) or ex b1 being Element of Seg a1 st
( a3 . b2 < a2 . b2 & ( b1 . b2 <= a3 . b2 or a2 . b2 <= b1 . b2 ) ) ) } ;
coherence
{ b1 where B is Element of REAL c1 : ( for b1 being Element of Seg c1 holds
( c2 . b2 <= b1 . b2 & b1 . b2 <= c3 . b2 ) or ex b1 being Element of Seg c1 st
( c3 . b2 < c2 . b2 & ( b1 . b2 <= c3 . b2 or c2 . b2 <= b1 . b2 ) ) ) } is non empty Subset of (REAL c1)
proof end;
end;

:: deftheorem Def7 defines cell CHAIN_1:def 7 :
for b1 being non zero Nat
for b2, b3 being Element of REAL b1 holds cell b2,b3 = { b4 where B is Element of REAL b1 : ( for b1 being Element of Seg b1 holds
( b2 . b5 <= b4 . b5 & b4 . b5 <= b3 . b5 ) or ex b1 being Element of Seg b1 st
( b3 . b5 < b2 . b5 & ( b4 . b5 <= b3 . b5 or b2 . b5 <= b4 . b5 ) ) ) } ;

theorem Th24: :: CHAIN_1:24
for b1 being non zero Nat
for b2, b3, b4 being Element of REAL b1 holds
( b2 in cell b3,b4 iff ( for b5 being Element of Seg b1 holds
( b3 . b5 <= b2 . b5 & b2 . b5 <= b4 . b5 ) or ex b5 being Element of Seg b1 st
( b4 . b5 < b3 . b5 & ( b2 . b5 <= b4 . b5 or b3 . b5 <= b2 . b5 ) ) ) )
proof end;

theorem Th25: :: CHAIN_1:25
for b1 being non zero Nat
for b2, b3, b4 being Element of REAL b1 st ( for b5 being Element of Seg b1 holds b2 . b5 <= b3 . b5 ) holds
( b4 in cell b2,b3 iff for b5 being Element of Seg b1 holds
( b2 . b5 <= b4 . b5 & b4 . b5 <= b3 . b5 ) )
proof end;

theorem Th26: :: CHAIN_1:26
for b1 being non zero Nat
for b2, b3, b4 being Element of REAL b1 st ex b5 being Element of Seg b1 st b2 . b5 < b3 . b5 holds
( b4 in cell b3,b2 iff ex b5 being Element of Seg b1 st
( b2 . b5 < b3 . b5 & ( b4 . b5 <= b2 . b5 or b3 . b5 <= b4 . b5 ) ) )
proof end;

theorem Th27: :: CHAIN_1:27
for b1 being non zero Nat
for b2, b3 being Element of REAL b1 holds
( b2 in cell b2,b3 & b3 in cell b2,b3 )
proof end;

theorem Th28: :: CHAIN_1:28
for b1 being non zero Nat
for b2 being Element of REAL b1 holds cell b2,b2 = {b2}
proof end;

theorem Th29: :: CHAIN_1:29
for b1 being non zero Nat
for b2, b3, b4, b5 being Element of REAL b1 st ( for b6 being Element of Seg b1 holds b2 . b6 <= b3 . b6 ) holds
( cell b4,b5 c= cell b2,b3 iff for b6 being Element of Seg b1 holds
( b2 . b6 <= b4 . b6 & b4 . b6 <= b5 . b6 & b5 . b6 <= b3 . b6 ) )
proof end;

theorem Th30: :: CHAIN_1:30
for b1 being non zero Nat
for b2, b3, b4, b5 being Element of REAL b1 st ( for b6 being Element of Seg b1 holds b2 . b6 < b3 . b6 ) holds
( cell b3,b2 c= cell b4,b5 iff for b6 being Element of Seg b1 holds
( b2 . b6 <= b5 . b6 & b5 . b6 < b4 . b6 & b4 . b6 <= b3 . b6 ) )
proof end;

theorem Th31: :: CHAIN_1:31
for b1 being non zero Nat
for b2, b3, b4, b5 being Element of REAL b1 st ( for b6 being Element of Seg b1 holds b2 . b6 <= b3 . b6 ) & ( for b6 being Element of Seg b1 holds b4 . b6 < b5 . b6 ) holds
( cell b2,b3 c= cell b5,b4 iff ex b6 being Element of Seg b1 st
( b3 . b6 <= b4 . b6 or b5 . b6 <= b2 . b6 ) )
proof end;

theorem Th32: :: CHAIN_1:32
for b1 being non zero Nat
for b2, b3, b4, b5 being Element of REAL b1 st ( for b6 being Element of Seg b1 holds b2 . b6 <= b3 . b6 or for b6 being Element of Seg b1 holds b2 . b6 > b3 . b6 ) holds
( cell b2,b3 = cell b4,b5 iff ( b2 = b4 & b3 = b5 ) )
proof end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
assume E35: c3 <= c1 ;
func cells c3,c2 -> non empty finite Subset-Family of (REAL a1) equals :Def8: :: CHAIN_1:def 8
{ (cell b1,b2) where B is Element of REAL a1, B is Element of REAL a1 : ( ex b1 being Subset of (Seg a1) st
( card b3 = a3 & ( for b2 being Element of Seg a1 holds
( ( b4 in b3 & b1 . b4 < b2 . b4 & [(b1 . b4),(b2 . b4)] is Gap of a2 . b4 ) or ( not b4 in b3 & b1 . b4 = b2 . b4 & b1 . b4 in a2 . b4 ) ) ) ) or ( a3 = a1 & ( for b1 being Element of Seg a1 holds
( b2 . b3 < b1 . b3 & [(b1 . b3),(b2 . b3)] is Gap of a2 . b3 ) ) ) ) } ;
coherence
{ (cell b1,b2) where B is Element of REAL c1, B is Element of REAL c1 : ( ex b1 being Subset of (Seg c1) st
( card b3 = c3 & ( for b2 being Element of Seg c1 holds
( ( b4 in b3 & b1 . b4 < b2 . b4 & [(b1 . b4),(b2 . b4)] is Gap of c2 . b4 ) or ( not b4 in b3 & b1 . b4 = b2 . b4 & b1 . b4 in c2 . b4 ) ) ) ) or ( c3 = c1 & ( for b1 being Element of Seg c1 holds
( b2 . b3 < b1 . b3 & [(b1 . b3),(b2 . b3)] is Gap of c2 . b3 ) ) ) ) } is non empty finite Subset-Family of (REAL c1)
proof end;
end;

:: deftheorem Def8 defines cells CHAIN_1:def 8 :
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Nat st b3 <= b1 holds
cells b3,b2 = { (cell b4,b5) where B is Element of REAL b1, B is Element of REAL b1 : ( ex b1 being Subset of (Seg b1) st
( card b6 = b3 & ( for b2 being Element of Seg b1 holds
( ( b7 in b6 & b4 . b7 < b5 . b7 & [(b4 . b7),(b5 . b7)] is Gap of b2 . b7 ) or ( not b7 in b6 & b4 . b7 = b5 . b7 & b4 . b7 in b2 . b7 ) ) ) ) or ( b3 = b1 & ( for b1 being Element of Seg b1 holds
( b5 . b6 < b4 . b6 & [(b4 . b6),(b5 . b6)] is Gap of b2 . b6 ) ) ) ) } ;

theorem Th33: :: CHAIN_1:33
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2 st b1 <= b2 holds
for b4 being Subset of (REAL b2) holds
( b4 in cells b1,b3 iff ex b5, b6 being Element of REAL b2 st
( b4 = cell b5,b6 & ( ex b7 being Subset of (Seg b2) st
( card b7 = b1 & ( for b8 being Element of Seg b2 holds
( ( b8 in b7 & b5 . b8 < b6 . b8 & [(b5 . b8),(b6 . b8)] is Gap of b3 . b8 ) or ( not b8 in b7 & b5 . b8 = b6 . b8 & b5 . b8 in b3 . b8 ) ) ) ) or ( b1 = b2 & ( for b7 being Element of Seg b2 holds
( b6 . b7 < b5 . b7 & [(b5 . b7),(b6 . b7)] is Gap of b3 . b7 ) ) ) ) ) )
proof end;

theorem Th34: :: CHAIN_1:34
for b1 being Nat
for b2 being non zero Nat
for b3, b4 being Element of REAL b2
for b5 being Grating of b2 st b1 <= b2 holds
( cell b3,b4 in cells b1,b5 iff ( ex b6 being Subset of (Seg b2) st
( card b6 = b1 & ( for b7 being Element of Seg b2 holds
( ( b7 in b6 & b3 . b7 < b4 . b7 & [(b3 . b7),(b4 . b7)] is Gap of b5 . b7 ) or ( not b7 in b6 & b3 . b7 = b4 . b7 & b3 . b7 in b5 . b7 ) ) ) ) or ( b1 = b2 & ( for b6 being Element of Seg b2 holds
( b4 . b6 < b3 . b6 & [(b3 . b6),(b4 . b6)] is Gap of b5 . b6 ) ) ) ) )
proof end;

theorem Th35: :: CHAIN_1:35
for b1 being Nat
for b2 being non zero Nat
for b3, b4 being Element of REAL b2
for b5 being Grating of b2 st b1 <= b2 & cell b3,b4 in cells b1,b5 & ex b6 being Element of Seg b2 st
( not ( b3 . b6 < b4 . b6 & [(b3 . b6),(b4 . b6)] is Gap of b5 . b6 ) & not ( b3 . b6 = b4 . b6 & b3 . b6 in b5 . b6 ) ) holds
for b6 being Element of Seg b2 holds
( b4 . b6 < b3 . b6 & [(b3 . b6),(b4 . b6)] is Gap of b5 . b6 )
proof end;

theorem Th36: :: CHAIN_1:36
for b1 being Nat
for b2 being non zero Nat
for b3, b4 being Element of REAL b2
for b5 being Grating of b2 st b1 <= b2 & cell b3,b4 in cells b1,b5 holds
for b6 being Element of Seg b2 holds
( b3 . b6 in b5 . b6 & b4 . b6 in b5 . b6 )
proof end;

theorem Th37: :: CHAIN_1:37
for b1 being Nat
for b2 being non zero Nat
for b3, b4 being Element of REAL b2
for b5 being Grating of b2 st b1 <= b2 & cell b3,b4 in cells b1,b5 & not for b6 being Element of Seg b2 holds b3 . b6 <= b4 . b6 holds
for b6 being Element of Seg b2 holds b4 . b6 < b3 . b6 by Th35;

theorem Th38: :: CHAIN_1:38
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Subset of (REAL b1) holds
( b3 in cells 0,b2 iff ex b4 being Element of REAL b1 st
( b3 = cell b4,b4 & ( for b5 being Element of Seg b1 holds b4 . b5 in b2 . b5 ) ) )
proof end;

theorem Th39: :: CHAIN_1:39
for b1 being non zero Nat
for b2, b3 being Element of REAL b1
for b4 being Grating of b1 holds
( cell b2,b3 in cells 0,b4 iff ( b2 = b3 & ( for b5 being Element of Seg b1 holds b2 . b5 in b4 . b5 ) ) )
proof end;

theorem Th40: :: CHAIN_1:40
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Subset of (REAL b1) holds
( b3 in cells b1,b2 iff ex b4, b5 being Element of REAL b1 st
( b3 = cell b4,b5 & ( for b6 being Element of Seg b1 holds [(b4 . b6),(b5 . b6)] is Gap of b2 . b6 ) & ( for b6 being Element of Seg b1 holds b4 . b6 < b5 . b6 or for b6 being Element of Seg b1 holds b5 . b6 < b4 . b6 ) ) )
proof end;

theorem Th41: :: CHAIN_1:41
for b1 being non zero Nat
for b2, b3 being Element of REAL b1
for b4 being Grating of b1 holds
( cell b2,b3 in cells b1,b4 iff ( ( for b5 being Element of Seg b1 holds [(b2 . b5),(b3 . b5)] is Gap of b4 . b5 ) & ( for b5 being Element of Seg b1 holds b2 . b5 < b3 . b5 or for b5 being Element of Seg b1 holds b3 . b5 < b2 . b5 ) ) )
proof end;

theorem Th42: :: CHAIN_1:42
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2 st b2 = b1 + 1 holds
for b4 being Subset of (REAL b2) holds
( b4 in cells b1,b3 iff ex b5, b6 being Element of REAL b2ex b7 being Element of Seg b2 st
( b4 = cell b5,b6 & b5 . b7 = b6 . b7 & b5 . b7 in b3 . b7 & ( for b8 being Element of Seg b2 st b8 <> b7 holds
( b5 . b8 < b6 . b8 & [(b5 . b8),(b6 . b8)] is Gap of b3 . b8 ) ) ) )
proof end;

theorem Th43: :: CHAIN_1:43
for b1 being Nat
for b2 being non zero Nat
for b3, b4 being Element of REAL b2
for b5 being Grating of b2 st b2 = b1 + 1 holds
( cell b3,b4 in cells b1,b5 iff ex b6 being Element of Seg b2 st
( b3 . b6 = b4 . b6 & b3 . b6 in b5 . b6 & ( for b7 being Element of Seg b2 st b7 <> b6 holds
( b3 . b7 < b4 . b7 & [(b3 . b7),(b4 . b7)] is Gap of b5 . b7 ) ) ) )
proof end;

theorem Th44: :: CHAIN_1:44
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Subset of (REAL b1) holds
( b3 in cells 1,b2 iff ex b4, b5 being Element of REAL b1ex b6 being Element of Seg b1 st
( b3 = cell b4,b5 & ( b4 . b6 < b5 . b6 or ( b1 = 1 & b5 . b6 < b4 . b6 ) ) & [(b4 . b6),(b5 . b6)] is Gap of b2 . b6 & ( for b7 being Element of Seg b1 st b7 <> b6 holds
( b4 . b7 = b5 . b7 & b4 . b7 in b2 . b7 ) ) ) )
proof end;

theorem Th45: :: CHAIN_1:45
for b1 being non zero Nat
for b2, b3 being Element of REAL b1
for b4 being Grating of b1 holds
( cell b2,b3 in cells 1,b4 iff ex b5 being Element of Seg b1 st
( ( b2 . b5 < b3 . b5 or ( b1 = 1 & b3 . b5 < b2 . b5 ) ) & [(b2 . b5),(b3 . b5)] is Gap of b4 . b5 & ( for b6 being Element of Seg b1 st b6 <> b5 holds
( b2 . b6 = b3 . b6 & b2 . b6 in b4 . b6 ) ) ) )
proof end;

theorem Th46: :: CHAIN_1:46
for b1, b2 being Nat
for b3 being non zero Nat
for b4, b5, b6, b7 being Element of REAL b3
for b8 being Grating of b3 st b1 <= b3 & b2 <= b3 & cell b4,b5 in cells b1,b8 & cell b6,b7 in cells b2,b8 & cell b4,b5 c= cell b6,b7 holds
for b9 being Element of Seg b3 holds
( ( b4 . b9 = b6 . b9 & b5 . b9 = b7 . b9 ) or ( b4 . b9 = b6 . b9 & b5 . b9 = b6 . b9 ) or ( b4 . b9 = b7 . b9 & b5 . b9 = b7 . b9 ) or ( b4 . b9 <= b5 . b9 & b7 . b9 < b6 . b9 & b7 . b9 <= b4 . b9 & b5 . b9 <= b6 . b9 ) )
proof end;

theorem Th47: :: CHAIN_1:47
for b1, b2 being Nat
for b3 being non zero Nat
for b4, b5, b6, b7 being Element of REAL b3
for b8 being Grating of b3 st b1 < b2 & b2 <= b3 & cell b4,b5 in cells b1,b8 & cell b6,b7 in cells b2,b8 & cell b4,b5 c= cell b6,b7 holds
ex b9 being Element of Seg b3 st
( ( b4 . b9 = b6 . b9 & b5 . b9 = b6 . b9 ) or ( b4 . b9 = b7 . b9 & b5 . b9 = b7 . b9 ) )
proof end;

theorem Th48: :: CHAIN_1:48
for b1 being non zero Nat
for b2, b3, b4, b5 being Element of REAL b1
for b6 being Grating of b1
for b7, b8 being Subset of (Seg b1) st cell b2,b3 c= cell b4,b5 & ( for b9 being Element of Seg b1 holds
( ( b9 in b7 & b2 . b9 < b3 . b9 & [(b2 . b9),(b3 . b9)] is Gap of b6 . b9 ) or ( not b9 in b7 & b2 . b9 = b3 . b9 & b2 . b9 in b6 . b9 ) ) ) & ( for b9 being Element of Seg b1 holds
( ( b9 in b8 & b4 . b9 < b5 . b9 & [(b4 . b9),(b5 . b9)] is Gap of b6 . b9 ) or ( not b9 in b8 & b4 . b9 = b5 . b9 & b4 . b9 in b6 . b9 ) ) ) holds
( b7 c= b8 & ( for b9 being Element of Seg b1 st ( b9 in b7 or not b9 in b8 ) holds
( b2 . b9 = b4 . b9 & b3 . b9 = b5 . b9 ) ) & ( for b9 being Element of Seg b1 st not b9 in b7 & b9 in b8 & not ( b2 . b9 = b4 . b9 & b3 . b9 = b4 . b9 ) holds
( b2 . b9 = b5 . b9 & b3 . b9 = b5 . b9 ) ) )
proof end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
mode Cell of a3,a2 is Element of cells a3,a2;
end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
mode Chain of a3,a2 is Subset of (cells a3,a2);
end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
func 0_ c3,c2 -> Chain of a3,a2 equals :: CHAIN_1:def 9
 {} ;
coherence
{} is Chain of c3,c2 by SUBSET_1:4;
end;

:: deftheorem Def9 defines 0_ CHAIN_1:def 9 :
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Nat holds 0_ b3,b2 = {} ;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
func Omega c2 -> Chain of a1,a2 equals :: CHAIN_1:def 10
 cells a1,a2;
coherence
cells c1,c2 is Chain of c1,c2
proof end;
end;

:: deftheorem Def10 defines Omega CHAIN_1:def 10 :
for b1 being non zero Nat
for b2 being Grating of b1 holds Omega b2 = cells b1,b2;

notation
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
let c4, c5 be Chain of c3,c2;
synonym c4 + c5 for c1 \+\ c2;
end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
let c4, c5 be Chain of c3,c2;
redefine func + as c4 + c5 -> Chain of a3,a2;
coherence
+ is Chain of c3,c2
proof end;
end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
func infinite-cell c2 -> Cell of a1,a2 means :Def11: :: CHAIN_1:def 11
ex b1, b2 being Element of REAL a1 st
( a3 = cell b1,b2 & ( for b3 being Element of Seg a1 holds
( b2 . b3 < b1 . b3 & [(b1 . b3),(b2 . b3)] is Gap of a2 . b3 ) ) );
existence
ex b1 being Cell of c1,c2ex b2, b3 being Element of REAL c1 st
( b1 = cell b2,b3 & ( for b4 being Element of Seg c1 holds
( b3 . b4 < b2 . b4 & [(b2 . b4),(b3 . b4)] is Gap of c2 . b4 ) ) )
proof end;
uniqueness
for b1, b2 being Cell of c1,c2 st ex b3, b4 being Element of REAL c1 st
( b1 = cell b3,b4 & ( for b5 being Element of Seg c1 holds
( b4 . b5 < b3 . b5 & [(b3 . b5),(b4 . b5)] is Gap of c2 . b5 ) ) ) & ex b3, b4 being Element of REAL c1 st
( b2 = cell b3,b4 & ( for b5 being Element of Seg c1 holds
( b4 . b5 < b3 . b5 & [(b3 . b5),(b4 . b5)] is Gap of c2 . b5 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines infinite-cell CHAIN_1:def 11 :
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Cell of b1,b2 holds
( b3 = infinite-cell b2 iff ex b4, b5 being Element of REAL b1 st
( b3 = cell b4,b5 & ( for b6 being Element of Seg b1 holds
( b5 . b6 < b4 . b6 & [(b4 . b6),(b5 . b6)] is Gap of b2 . b6 ) ) ) );

theorem Th49: :: CHAIN_1:49
for b1 being non zero Nat
for b2, b3 being Element of REAL b1
for b4 being Grating of b1 st cell b2,b3 is Cell of b1,b4 holds
( cell b2,b3 = infinite-cell b4 iff for b5 being Element of Seg b1 holds b3 . b5 < b2 . b5 )
proof end;

theorem Th50: :: CHAIN_1:50
for b1 being non zero Nat
for b2, b3 being Element of REAL b1
for b4 being Grating of b1 holds
( cell b2,b3 = infinite-cell b4 iff for b5 being Element of Seg b1 holds
( b3 . b5 < b2 . b5 & [(b2 . b5),(b3 . b5)] is Gap of b4 . b5 ) )
proof end;

scheme :: CHAIN_1:sch 4
s4{ F1() -> non zero Nat, F2() -> Grating of F1(), F3() -> Nat, F4() -> Chain of F3(),F2(), P1[ set ] } :
P1[F4()]
provided
E52: P1[ 0_ F3(),F2()] and
E53: for b1 being Cell of F3(),F2() st b1 in F4() holds
P1[{b1}] and
E54: for b1, b2 being Chain of F3(),F2() st b1 c= F4() & b2 c= F4() & P1[b1] & P1[b2] holds
P1[b1 + b2]
proof end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
let c4 be Cell of c3,c2;
func star c4 -> Chain of (a3 + 1),a2 equals :: CHAIN_1:def 12
{ b1 where B is Cell of (a3 + 1),a2 : a4 c= b1 } ;
coherence
{ b1 where B is Cell of (c3 + 1),c2 : c4 c= b1 } is Chain of (c3 + 1),c2
proof end;
end;

:: deftheorem Def12 defines star CHAIN_1:def 12 :
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Nat
for b4 being Cell of b3,b2 holds star b4 = { b5 where B is Cell of (b3 + 1),b2 : b4 c= b5 } ;

theorem Th51: :: CHAIN_1:51
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2
for b4 being Cell of b1,b3
for b5 being Cell of (b1 + 1),b3 holds
( b5 in star b4 iff b4 c= b5 )
proof end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
let c4 be Chain of (c3 + 1),c2;
func del c4 -> Chain of a3,a2 equals :: CHAIN_1:def 13
{ b1 where B is Cell of a3,a2 : ( a3 + 1 <= a1 & not card ((star b1) /\ a4) is even ) } ;
coherence
{ b1 where B is Cell of c3,c2 : ( c3 + 1 <= c1 & not card ((star b1) /\ c4) is even ) } is Chain of c3,c2
proof end;
end;

:: deftheorem Def13 defines del CHAIN_1:def 13 :
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Nat
for b4 being Chain of (b3 + 1),b2 holds del b4 = { b5 where B is Cell of b3,b2 : ( b3 + 1 <= b1 & not card ((star b5) /\ b4) is even ) } ;

notation
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
let c4 be Chain of (c3 + 1),c2;
synonym . c4 for del c4;
end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
let c4 be Chain of (c3 + 1),c2;
let c5 be Chain of c3,c2;
pred c5 bounds c4 means :: CHAIN_1:def 14
a5 = del a4;
end;

:: deftheorem Def14 defines bounds CHAIN_1:def 14 :
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Nat
for b4 being Chain of (b3 + 1),b2
for b5 being Chain of b3,b2 holds
( b5 bounds b4 iff b5 = del b4 );

theorem Th52: :: CHAIN_1:52
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2
for b4 being Cell of b1,b3
for b5 being Chain of (b1 + 1),b3 holds
( b4 in del b5 iff ( b1 + 1 <= b2 & not card ((star b4) /\ b5) is even ) )
proof end;

theorem Th53: :: CHAIN_1:53
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2 st b1 + 1 > b2 holds
for b4 being Chain of (b1 + 1),b3 holds del b4 = 0_ b1,b3
proof end;

theorem Th54: :: CHAIN_1:54
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2 st b1 + 1 <= b2 holds
for b4 being Cell of b1,b3
for b5 being Cell of (b1 + 1),b3 holds
( b4 in del {b5} iff b4 c= b5 )
proof end;

theorem Th55: :: CHAIN_1:55
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2 st b2 = b1 + 1 holds
for b4 being Cell of b1,b3 holds card (star b4) = 2
proof end;

theorem Th56: :: CHAIN_1:56
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Cell of (0 + 1),b2 holds card (del {b3}) = 2
proof end;

theorem Th57: :: CHAIN_1:57
for b1 being non zero Nat
for b2 being Grating of b1 holds
( Omega b2 = (0_ b1,b2) ` & 0_ b1,b2 = (Omega b2) ` )
proof end;

theorem Th58: :: CHAIN_1:58
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2
for b4 being Chain of b1,b3 holds b4 + (0_ b1,b3) = b4 ;

theorem Th59: :: CHAIN_1:59
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2
for b4 being Chain of b1,b3 holds b4 + b4 = 0_ b1,b3 by XBOOLE_1:92;

theorem Th60: :: CHAIN_1:60
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Chain of b1,b2 holds b3 ` = b3 + (Omega b2)
proof end;

theorem Th61: :: CHAIN_1:61
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2 holds del (0_ (b1 + 1),b3) = 0_ b1,b3
proof end;

theorem Th62: :: CHAIN_1:62
for b1 being Nat
for b2 being Grating of b1 + 1 holds del (Omega b2) = 0_ b1,b2
proof end;

theorem Th63: :: CHAIN_1:63
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2
for b4, b5 being Chain of (b1 + 1),b3 holds del (b4 + b5) = (del b4) + (del b5)
proof end;

theorem Th64: :: CHAIN_1:64
for b1 being Nat
for b2 being Grating of b1 + 1
for b3 being Chain of (b1 + 1),b2 holds del (b3 ` ) = del b3
proof end;

theorem Th65: :: CHAIN_1:65
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2
for b4 being Chain of ((b1 + 1) + 1),b3 holds del (del b4) = 0_ b1,b3
proof end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
mode Cycle of c3,c2 -> Chain of a3,a2 means :Def15: :: CHAIN_1:def 15
( ( a3 = 0 & card a4 is even ) or ex b1 being Nat st
( a3 = b1 + 1 & ex b2 being Chain of (b1 + 1),a2 st
( b2 = a4 & del b2 = 0_ b1,a2 ) ) );
existence
ex b1 being Chain of c3,c2 st
( ( c3 = 0 & card b1 is even ) or ex b2 being Nat st
( c3 = b2 + 1 & ex b3 being Chain of (b2 + 1),c2 st
( b3 = b1 & del b3 = 0_ b2,c2 ) ) )
proof end;
end;

:: deftheorem Def15 defines Cycle CHAIN_1:def 15 :
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Nat
for b4 being Chain of b3,b2 holds
( b4 is Cycle of b3,b2 iff ( ( b3 = 0 & card b4 is even ) or ex b5 being Nat st
( b3 = b5 + 1 & ex b6 being Chain of (b5 + 1),b2 st
( b6 = b4 & del b6 = 0_ b5,b2 ) ) ) );

theorem Th66: :: CHAIN_1:66
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2
for b4 being Chain of (b1 + 1),b3 holds
( b4 is Cycle of b1 + 1,b3 iff del b4 = 0_ b1,b3 )
proof end;

theorem Th67: :: CHAIN_1:67
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2 st b1 > b2 holds
for b4 being Chain of b1,b3 holds b4 is Cycle of b1,b3
proof end;

theorem Th68: :: CHAIN_1:68
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Chain of 0,b2 holds
( b3 is Cycle of 0,b2 iff card b3 is even )
proof end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
let c4 be Cycle of c3 + 1,c2;
redefine func del c4 -> Chain of a3,a2 equals :: CHAIN_1:def 16
 0_ a3,a2;
compatibility
for b1 being Chain of c3,c2 holds
( b1 = del c4 iff b1 = 0_ c3,c2 ) by Th66;
end;

:: deftheorem Def16 defines del CHAIN_1:def 16 :
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Nat
for b4 being Cycle of b3 + 1,b2 holds del b4 = 0_ b3,b2;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
redefine func 0_ as 0_ c3,c2 -> Cycle of a3,a2;
coherence
0_ c3,c2 is Cycle of c3,c2
proof end;
end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
redefine func Omega as Omega c2 -> Cycle of a1,a2;
coherence
Omega c2 is Cycle of c1,c2
proof end;
end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
let c4, c5 be Cycle of c3,c2;
redefine func + as c4 + c5 -> Cycle of a3,a2;
coherence
+ is Cycle of c3,c2
proof end;
end;

theorem Th69: :: CHAIN_1:69
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Cycle of b1,b2 holds b3 ` is Cycle of b1,b2
proof end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
let c4 be Chain of (c3 + 1),c2;
redefine func del as del c4 -> Cycle of a3,a2;
coherence
del c4 is Cycle of c3,c2
proof end;
end;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
func Chains c3,c2 -> strict AbGroup means :Def17: :: CHAIN_1:def 17
( the carrier of a4 = bool (cells a3,a2) & 0. a4 = 0_ a3,a2 & ( for b1, b2 being Element of a4
for b3, b4 being Chain of a3,a2 st b1 = b3 & b2 = b4 holds
b1 + b2 = b3 + b4 ) );
existence
ex b1 being strict AbGroup st
( the carrier of b1 = bool (cells c3,c2) & 0. b1 = 0_ c3,c2 & ( for b2, b3 being Element of b1
for b4, b5 being Chain of c3,c2 st b2 = b4 & b3 = b5 holds
b2 + b3 = b4 + b5 ) )
proof end;
uniqueness
for b1, b2 being strict AbGroup st the carrier of b1 = bool (cells c3,c2) & 0. b1 = 0_ c3,c2 & ( for b3, b4 being Element of b1
for b5, b6 being Chain of c3,c2 st b3 = b5 & b4 = b6 holds
b3 + b4 = b5 + b6 ) & the carrier of b2 = bool (cells c3,c2) & 0. b2 = 0_ c3,c2 & ( for b3, b4 being Element of b2
for b5, b6 being Chain of c3,c2 st b3 = b5 & b4 = b6 holds
b3 + b4 = b5 + b6 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines Chains CHAIN_1:def 17 :
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Nat
for b4 being strict AbGroup holds
( b4 = Chains b3,b2 iff ( the carrier of b4 = bool (cells b3,b2) & 0. b4 = 0_ b3,b2 & ( for b5, b6 being Element of b4
for b7, b8 being Chain of b3,b2 st b5 = b7 & b6 = b8 holds
b5 + b6 = b7 + b8 ) ) );

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
mode GrChain of a3,a2 is Element of (Chains a3,a2);
end;

theorem Th70: :: CHAIN_1:70
for b1 being Nat
for b2 being non zero Nat
for b3 being Grating of b2
for b4 being set holds
( b4 is Chain of b1,b3 iff b4 is GrChain of b1,b3 ) by Def17;

definition
let c1 be non zero Nat;
let c2 be Grating of c1;
let c3 be Nat;
func del c3,c2 -> Homomorphism of Chains (a3 + 1),a2, Chains a3,a2 means :: CHAIN_1:def 18
for b1 being Element of (Chains (a3 + 1),a2)
for b2 being Chain of (a3 + 1),a2 st b1 = b2 holds
a4 . b1 = del b2;
existence
ex b1 being Homomorphism of Chains (c3 + 1),c2, Chains c3,c2 st
for b2 being Element of (Chains (c3 + 1),c2)
for b3 being Chain of (c3 + 1),c2 st b2 = b3 holds
b1 . b2 = del b3
proof end;
uniqueness
for b1, b2 being Homomorphism of Chains (c3 + 1),c2, Chains c3,c2 st ( for b3 being Element of (Chains (c3 + 1),c2)
for b4 being Chain of (c3 + 1),c2 st b3 = b4 holds
b1 . b3 = del b4 ) & ( for b3 being Element of (Chains (c3 + 1),c2)
for b4 being Chain of (c3 + 1),c2 st b3 = b4 holds
b2 . b3 = del b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines del CHAIN_1:def 18 :
for b1 being non zero Nat
for b2 being Grating of b1
for b3 being Nat
for b4 being Homomorphism of Chains (b3 + 1),b2, Chains b3,b2 holds
( b4 = del b3,b2 iff for b5 being Element of (Chains (b3 + 1),b2)
for b6 being Chain of (b3 + 1),b2 st b5 = b6 holds
b4 . b5 = del b6 );