let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is BiFunction of (ConsecutiveSet2 A,O),L
let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is BiFunction of (ConsecutiveSet2 A,O),L
let d be BiFunction of A,L; :: thesis: for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is BiFunction of (ConsecutiveSet2 A,O),L
let q be QuadrSeq of d; :: thesis: for O being Ordinal holds ConsecutiveDelta2 q,O is BiFunction of (ConsecutiveSet2 A,O),L
let O be Ordinal; :: thesis: ConsecutiveDelta2 q,O is BiFunction of (ConsecutiveSet2 A,O),L
defpred S₁[ Ordinal] means ConsecutiveDelta2 q,$1 is BiFunction of (ConsecutiveSet2 A,$1),L;
A1: S₁[ {} ]

proof

( ConsecutiveDelta2 q,{} = d & ConsecutiveSet2 A,{} = A ) by Th15, Th19;
hence S₁[ {} ] ; :: thesis: verum

end;

A2: for O1 being Ordinal st S₁[O1] holds
S₁[ succ O1]

proof

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
assume ConsecutiveDelta2 q,O1 is BiFunction of (ConsecutiveSet2 A,O1),L ; :: thesis: S₁[ succ O1]
then reconsider CD = ConsecutiveDelta2 q,O1 as BiFunction of (ConsecutiveSet2 A,O1),L ;
A3: ConsecutiveSet2 A,(succ O1) = new_set2 (ConsecutiveSet2 A,O1) by Th16;
ConsecutiveDelta2 q,(succ O1) = new_bi_fun2 (BiFun (ConsecutiveDelta2 q,O1),(ConsecutiveSet2 A,O1),L),(Quadr2 q,O1) by Th20
.= new_bi_fun2 CD,(Quadr2 q,O1) by LATTICE5:def 16 ;
hence S₁[ succ O1] by A3; :: thesis: verum

end;

A4: for O1 being Ordinal st O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) holds
S₁[O1]

proof

let O1 be Ordinal; :: thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) implies S₁[O1] )
assume A5: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
ConsecutiveDelta2 q,O2 is BiFunction of (ConsecutiveSet2 A,O2),L ) ) ; :: thesis: S₁[O1]
deffunc H₁( Ordinal) -> set = ConsecutiveDelta2 q,$1;
consider Ls being T-Sequence such that
A6: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ls . O2 = H₁(O2) ) ) from ORDINAL2:sch 2();
A7: ConsecutiveDelta2 q,O1 = union (rng Ls) by A5, A6, Th21;
deffunc H₂( Ordinal) -> set = ConsecutiveSet2 A,$1;
consider Ts being T-Sequence such that
A8: ( dom Ts = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ts . O2 = H₂(O2) ) ) from ORDINAL2:sch 2();
set CS = ConsecutiveSet2 A,O1;
set Y = the carrier of L;
set X = [:(ConsecutiveSet2 A,O1),(ConsecutiveSet2 A,O1):];
set f = union (rng Ls);
A9: for O, O2 being Ordinal st O c= O2 & O2 in dom Ls holds
Ls . O c= Ls . O2

proof

let O be Ordinal; :: thesis: for O2 being Ordinal st O c= O2 & O2 in dom Ls holds
Ls . O c= Ls . O2
defpred S₂[ Ordinal] means ( O c= $1 & $1 in dom Ls implies Ls . O c= Ls . $1 );
A10: S₂[ {} ] ;
A11: for O1 being Ordinal st S₂[O1] holds
S₂[ succ O1]

proof

let O2 be Ordinal; :: thesis: ( S₂[O2] implies S₂[ succ O2] )
assume A12: ( O c= O2 & O2 in dom Ls implies Ls . O c= Ls . O2 ) ; :: thesis: S₂[ succ O2]
assume that
A13: O c= succ O2 and
A14: succ O2 in dom Ls ; :: thesis: Ls . O c= Ls . (succ O2)

per cases ( O = succ O2 or O <> succ O2 ) ;

suppose O = succ O2 ; :: thesis: Ls . O c= Ls . (succ O2)

hence Ls . O c= Ls . (succ O2) ; :: thesis: verum

end;

suppose O <> succ O2 ; :: thesis: Ls . O c= Ls . (succ O2)

then O c< succ O2 by A13, XBOOLE_0:def 8;
then A15: O in succ O2 by ORDINAL1:21;
A16: O2 in succ O2 by ORDINAL1:10;
then O2 in dom Ls by A14, ORDINAL1:19;
then reconsider Def8 = ConsecutiveDelta2 q,O2 as BiFunction of (ConsecutiveSet2 A,O2),L by A5, A6;
Ls . (succ O2) = ConsecutiveDelta2 q,(succ O2) by A6, A14
.= new_bi_fun2 (BiFun (ConsecutiveDelta2 q,O2),(ConsecutiveSet2 A,O2),L),(Quadr2 q,O2) by Th20
.= new_bi_fun2 Def8,(Quadr2 q,O2) by LATTICE5:def 16 ;
then ConsecutiveDelta2 q,O2 c= Ls . (succ O2) by Th14;
then Ls . O2 c= Ls . (succ O2) by A6, A14, A16, ORDINAL1:19;
hence Ls . O c= Ls . (succ O2) by A12, A14, A15, A16, ORDINAL1:19, ORDINAL1:34, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

A17: for O1 being Ordinal st O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₂[O2] ) holds
S₂[O1]

proof

let O2 be Ordinal; :: thesis: ( O2 <> {} & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S₂[O2] ) implies S₂[O2] )
assume that
A18: ( O2 <> {} & O2 is limit_ordinal ) and
for O3 being Ordinal st O3 in O2 & O c= O3 & O3 in dom Ls holds
Ls . O c= Ls . O3 ; :: thesis: S₂[O2]
assume that
A19: O c= O2 and
A20: O2 in dom Ls ; :: thesis: Ls . O c= Ls . O2
deffunc H₃( Ordinal) -> set = ConsecutiveDelta2 q,$1;
consider Lt being T-Sequence such that
A21: ( dom Lt = O2 & ( for O3 being Ordinal st O3 in O2 holds
Lt . O3 = H₃(O3) ) ) from ORDINAL2:sch 2();
A22: Ls . O2 = ConsecutiveDelta2 q,O2 by A6, A20
.= union (rng Lt) by A18, A21, Th21 ;

per cases ( O = O2 or O <> O2 ) ;

suppose O = O2 ; :: thesis: Ls . O c= Ls . O2

hence Ls . O c= Ls . O2 ; :: thesis: verum

end;

suppose O <> O2 ; :: thesis: Ls . O c= Ls . O2

then A23: O c< O2 by A19, XBOOLE_0:def 8;
then A24: O in O2 by ORDINAL1:21;
then Ls . O = ConsecutiveDelta2 q,O by A6, A20, ORDINAL1:19
.= Lt . O by A21, A23, ORDINAL1:21 ;
then Ls . O in rng Lt by A21, A24, FUNCT_1:def 5;
hence Ls . O c= Ls . O2 by A22, ZFMISC_1:92; :: thesis: verum

end;

end;

end;

thus for O being Ordinal holds S₂[O] from ORDINAL2:sch 1(A10, A11, A17); :: thesis: verum

end;

for x, y being set st x in rng Ls & y in rng Ls holds
x,y are_c=-comparable

proof

let x, y be set ; :: thesis: ( x in rng Ls & y in rng Ls implies x,y are_c=-comparable )
assume A25: ( x in rng Ls & y in rng Ls ) ; :: thesis: x,y are_c=-comparable
then consider o1 being set such that
A26: ( o1 in dom Ls & Ls . o1 = x ) by FUNCT_1:def 5;
consider o2 being set such that
A27: ( o2 in dom Ls & Ls . o2 = y ) by A25, FUNCT_1:def 5;
reconsider o1' = o1, o2' = o2 as Ordinal by A26, A27;
( o1' c= o2' or o2' c= o1' ) ;
then ( x c= y or y c= x ) by A9, A26, A27;
hence x,y are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;

then A28: rng Ls is c=-linear by ORDINAL1:def 9;
rng Ls c= PFuncs [:(ConsecutiveSet2 A,O1),(ConsecutiveSet2 A,O1):],the carrier of L

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng Ls or z in PFuncs [:(ConsecutiveSet2 A,O1),(ConsecutiveSet2 A,O1):],the carrier of L )
assume z in rng Ls ; :: thesis: z in PFuncs [:(ConsecutiveSet2 A,O1),(ConsecutiveSet2 A,O1):],the carrier of L
then consider o being set such that
A29: ( o in dom Ls & z = Ls . o ) by FUNCT_1:def 5;
reconsider o = o as Ordinal by A29;
Ls . o = ConsecutiveDelta2 q,o by A6, A29;
then reconsider h = Ls . o as BiFunction of (ConsecutiveSet2 A,o),L by A5, A6, A29;
A30: dom h = [:(ConsecutiveSet2 A,o),(ConsecutiveSet2 A,o):] by FUNCT_2:def 1;
A31: rng h c= the carrier of L ;
o c= O1 by A6, A29, ORDINAL1:def 2;
then ConsecutiveSet2 A,o c= ConsecutiveSet2 A,O1 by Th22;
then dom h c= [:(ConsecutiveSet2 A,O1),(ConsecutiveSet2 A,O1):] by A30, ZFMISC_1:119;
hence z in PFuncs [:(ConsecutiveSet2 A,O1),(ConsecutiveSet2 A,O1):],the carrier of L by A29, A31, PARTFUN1:def 5; :: thesis: verum

end;

then union (rng Ls) in PFuncs [:(ConsecutiveSet2 A,O1),(ConsecutiveSet2 A,O1):],the carrier of L by A28, HAHNBAN:13;
then consider g being Function such that
A32: ( union (rng Ls) = g & dom g c= [:(ConsecutiveSet2 A,O1),(ConsecutiveSet2 A,O1):] & rng g c= the carrier of L ) by PARTFUN1:def 5;
reconsider f = union (rng Ls) as Function by A32;
Ls is Function-yielding

proof

let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom Ls or Ls . x is set )
assume A33: x in dom Ls ; :: thesis: Ls . x is set
then reconsider o = x as Ordinal ;
Ls . o = ConsecutiveDelta2 q,o by A6, A33;
hence Ls . x is set by A5, A6, A33; :: thesis: verum

end;

then reconsider LsF = Ls as Function-yielding Function ;
A34: dom f = union (rng (doms LsF)) by LATTICE5:1;
reconsider o1 = O1 as non empty Ordinal by A5;
set YY = { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } ;
A35: rng (doms Ls) = { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum }

proof

thus rng (doms Ls) c= { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } :: according to XBOOLE_0:def 10 :: thesis: { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } c= rng (doms Ls)

proof

let Z be set ; :: according to TARSKI:def 3 :: thesis: ( not Z in rng (doms Ls) or Z in { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } )
assume Z in rng (doms Ls) ; :: thesis: Z in { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum }
then consider o being set such that
A36: ( o in dom (doms Ls) & Z = (doms Ls) . o ) by FUNCT_1:def 5;
A37: o in dom LsF by A36, FUNCT_6:89;
then reconsider o' = o as Element of o1 by A6;
Ls . o' = ConsecutiveDelta2 q,o' by A6;
then reconsider ls = Ls . o' as BiFunction of (ConsecutiveSet2 A,o'),L by A5;
Z = dom ls by A36, A37, FUNCT_6:31
.= [:(ConsecutiveSet2 A,o'),(ConsecutiveSet2 A,o'):] by FUNCT_2:def 1 ;
hence Z in { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } ; :: thesis: verum

end;

let Z be set ; :: according to TARSKI:def 3 :: thesis: ( not Z in { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } or Z in rng (doms Ls) )
assume Z in { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } ; :: thesis: Z in rng (doms Ls)
then consider o being Element of o1 such that
A38: Z = [:(ConsecutiveSet2 A,o),(ConsecutiveSet2 A,o):] ;
o in dom LsF by A6;
then A39: o in dom (doms LsF) by FUNCT_6:89;
Ls . o = ConsecutiveDelta2 q,o by A6;
then reconsider ls = Ls . o as BiFunction of (ConsecutiveSet2 A,o),L by A5;
Z = dom ls by A38, FUNCT_2:def 1
.= (doms Ls) . o by A6, FUNCT_6:31 ;
hence Z in rng (doms Ls) by A39, FUNCT_1:def 5; :: thesis: verum

end;

{} in O1 by A5, ORDINAL3:10;
then reconsider RTs = rng Ts as non empty set by A8, FUNCT_1:12;
for x, y being set st x in RTs & y in RTs holds
x,y are_c=-comparable

proof

let x, y be set ; :: thesis: ( x in RTs & y in RTs implies x,y are_c=-comparable )
assume A40: ( x in RTs & y in RTs ) ; :: thesis: x,y are_c=-comparable
then consider o1 being set such that
A41: ( o1 in dom Ts & Ts . o1 = x ) by FUNCT_1:def 5;
consider o2 being set such that
A42: ( o2 in dom Ts & Ts . o2 = y ) by A40, FUNCT_1:def 5;
reconsider o1' = o1, o2' = o2 as Ordinal by A41, A42;
A43: Ts . o1' = ConsecutiveSet2 A,o1' by A8, A41;
A44: Ts . o2' = ConsecutiveSet2 A,o2' by A8, A42;
( o1' c= o2' or o2' c= o1' ) ;
then ( x c= y or y c= x ) by A41, A42, A43, A44, Th22;
hence x,y are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;

then A45: RTs is c=-linear by ORDINAL1:def 9;
A46: { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } = { [:a,a:] where a is Element of RTs : a in RTs }

proof

set XX = { [:a,a:] where a is Element of RTs : a in RTs } ;
thus { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } c= { [:a,a:] where a is Element of RTs : a in RTs } :: according to XBOOLE_0:def 10 :: thesis: { [:a,a:] where a is Element of RTs : a in RTs } c= { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum }

proof

let Z be set ; :: according to TARSKI:def 3 :: thesis: ( not Z in { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } or Z in { [:a,a:] where a is Element of RTs : a in RTs } )
assume Z in { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } ; :: thesis: Z in { [:a,a:] where a is Element of RTs : a in RTs }
then consider o being Element of o1 such that
A47: Z = [:(ConsecutiveSet2 A,o),(ConsecutiveSet2 A,o):] ;
Ts . o = ConsecutiveSet2 A,o by A8;
then reconsider CoS = ConsecutiveSet2 A,o as Element of RTs by A8, FUNCT_1:def 5;
Z = [:CoS,CoS:] by A47;
hence Z in { [:a,a:] where a is Element of RTs : a in RTs } ; :: thesis: verum

end;

let Z be set ; :: according to TARSKI:def 3 :: thesis: ( not Z in { [:a,a:] where a is Element of RTs : a in RTs } or Z in { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } )
assume Z in { [:a,a:] where a is Element of RTs : a in RTs } ; :: thesis: Z in { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum }
then consider a being Element of RTs such that
A48: ( Z = [:a,a:] & a in RTs ) ;
consider o being set such that
A49: ( o in dom Ts & a = Ts . o ) by FUNCT_1:def 5;
reconsider o' = o as Ordinal by A49;
A50: a = ConsecutiveSet2 A,o' by A8, A49;
consider O being Element of o1 such that
A51: O = o' by A8, A49;
thus Z in { [:(ConsecutiveSet2 A,O2),(ConsecutiveSet2 A,O2):] where O2 is Element of o1 : verum } by A48, A50, A51; :: thesis: verum

end;

[:(ConsecutiveSet2 A,O1),(ConsecutiveSet2 A,O1):] = [:(union (rng Ts)),(ConsecutiveSet2 A,O1):] by A5, A8, Th17
.= [:(union RTs),(union RTs):] by A5, A8, Th17
.= dom f by A34, A35, A45, A46, LATTICE5:3 ;
hence S₁[O1] by A7, A32, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A1, A2, A4);
hence ConsecutiveDelta2 q,O is BiFunction of (ConsecutiveSet2 A,O),L ; :: thesis: verum