let L be lower-bounded modular LATTICE; for S being ExtensionSeq2 of the carrier of L, BasicDF L
for FS being non empty set
for FD being distance_function of FS,L
for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2 being Element of FS st
( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )
let S be ExtensionSeq2 of the carrier of L, BasicDF L; for FS being non empty set
for FD being distance_function of FS,L
for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2 being Element of FS st
( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )
let FS be non empty set ; for FD being distance_function of FS,L
for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2 being Element of FS st
( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )
let FD be distance_function of FS,L; for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2 being Element of FS st
( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )
let x, y be Element of FS; for a, b being Element of L st FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2 being Element of FS st
( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )
let a, b be Element of L; ( FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b implies ex z1, z2 being Element of FS st
( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a ) )
assume that
A1:
FS = union { ((S . i) `1) where i is Element of NAT : verum }
and
A2:
FD = union { ((S . i) `2) where i is Element of NAT : verum }
and
A3:
FD . (x,y) <= a "\/" b
; ex z1, z2 being Element of FS st
( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )
(S . 0) `1 in { ((S . i) `1) where i is Element of NAT : verum }
;
then reconsider X = { ((S . i) `1) where i is Element of NAT : verum } as non empty set ;
consider x1 being set such that
A4:
x in x1
and
A5:
x1 in X
by A1, TARSKI:def 4;
consider k being Element of NAT such that
A6:
x1 = (S . k) `1
by A5;
consider A1 being non empty set , d1 being distance_function of A1,L, Aq1 being non empty set , dq1 being distance_function of Aq1,L such that
A7:
Aq1,dq1 is_extension2_of A1,d1
and
A8:
S . k = [A1,d1]
and
A9:
S . (k + 1) = [Aq1,dq1]
by Def11;
A10:
[A1,d1] `1 = A1
;
A11:
x in A1
by A4, A6, A8;
[A1,d1] `2 = d1
;
then
d1 in { ((S . i) `2) where i is Element of NAT : verum }
by A8;
then A12:
d1 c= FD
by A2, ZFMISC_1:74;
A13:
[Aq1,dq1] `1 = Aq1
;
then
Aq1 in { ((S . i) `1) where i is Element of NAT : verum }
by A9;
then A14:
Aq1 c= FS
by A1, ZFMISC_1:74;
[Aq1,dq1] `2 = dq1
;
then
dq1 in { ((S . i) `2) where i is Element of NAT : verum }
by A9;
then A15:
dq1 c= FD
by A2, ZFMISC_1:74;
consider y1 being set such that
A16:
y in y1
and
A17:
y1 in X
by A1, TARSKI:def 4;
consider l being Element of NAT such that
A18:
y1 = (S . l) `1
by A17;
consider A2 being non empty set , d2 being distance_function of A2,L, Aq2 being non empty set , dq2 being distance_function of Aq2,L such that
A19:
Aq2,dq2 is_extension2_of A2,d2
and
A20:
S . l = [A2,d2]
and
A21:
S . (l + 1) = [Aq2,dq2]
by Def11;
A22:
[A2,d2] `1 = A2
;
A23:
y in A2
by A16, A18, A20;
[A2,d2] `2 = d2
;
then
d2 in { ((S . i) `2) where i is Element of NAT : verum }
by A20;
then A24:
d2 c= FD
by A2, ZFMISC_1:74;
A25:
[Aq2,dq2] `1 = Aq2
;
then
Aq2 in { ((S . i) `1) where i is Element of NAT : verum }
by A21;
then A26:
Aq2 c= FS
by A1, ZFMISC_1:74;
[Aq2,dq2] `2 = dq2
;
then
dq2 in { ((S . i) `2) where i is Element of NAT : verum }
by A21;
then A27:
dq2 c= FD
by A2, ZFMISC_1:74;
per cases
( k <= l or l <= k )
;
suppose
k <= l
;
ex z1, z2 being Element of FS st
( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )then
A1 c= A2
by A10, A22, Th30, A8, A20;
then reconsider x9 =
x,
y9 =
y as
Element of
A2 by A11, A16, A18, A20;
A2 c= Aq2
by A22, A25, Th30, A20, A21, NAT_1:11;
then reconsider x99 =
x9,
y99 =
y9 as
Element of
Aq2 ;
dom d2 = [:A2,A2:]
by FUNCT_2:def 1;
then A28:
FD . (
x,
y) =
d2 . [x9,y9]
by A24, GRFUNC_1:2
.=
d2 . (
x9,
y9)
;
then consider z1,
z2 being
Element of
Aq2 such that A29:
dq2 . (
x,
z1)
= a
and A30:
dq2 . (
z1,
z2)
= ((d2 . (x9,y9)) "\/" a) "/\" b
and A31:
dq2 . (
z2,
y)
= a
by A3, A19, Th29;
reconsider z19 =
z1,
z29 =
z2 as
Element of
FS by A26;
take
z19
;
ex z2 being Element of FS st
( FD . (x,z19) = a & FD . (z19,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )take
z29
;
( FD . (x,z19) = a & FD . (z19,z29) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z29,y) = a )A32:
dom dq2 = [:Aq2,Aq2:]
by FUNCT_2:def 1;
hence FD . (
x,
z19) =
dq2 . [x99,z1]
by A27, GRFUNC_1:2
.=
a
by A29
;
( FD . (z19,z29) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z29,y) = a )thus FD . (
z19,
z29) =
dq2 . [z1,z2]
by A27, A32, GRFUNC_1:2
.=
((FD . (x,y)) "\/" a) "/\" b
by A28, A30
;
FD . (z29,y) = athus FD . (
z29,
y) =
dq2 . [z2,y99]
by A27, A32, GRFUNC_1:2
.=
a
by A31
;
verum end; suppose
l <= k
;
ex z1, z2 being Element of FS st
( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )then
A2 c= A1
by A10, A22, Th30, A8, A20;
then reconsider x9 =
x,
y9 =
y as
Element of
A1 by A4, A6, A8, A23;
A1 c= Aq1
by A10, A13, Th30, A8, A9, NAT_1:11;
then reconsider x99 =
x9,
y99 =
y9 as
Element of
Aq1 ;
dom d1 = [:A1,A1:]
by FUNCT_2:def 1;
then A33:
FD . (
x,
y) =
d1 . [x9,y9]
by A12, GRFUNC_1:2
.=
d1 . (
x9,
y9)
;
then consider z1,
z2 being
Element of
Aq1 such that A34:
dq1 . (
x,
z1)
= a
and A35:
dq1 . (
z1,
z2)
= ((d1 . (x9,y9)) "\/" a) "/\" b
and A36:
dq1 . (
z2,
y)
= a
by A3, A7, Th29;
reconsider z19 =
z1,
z29 =
z2 as
Element of
FS by A14;
take
z19
;
ex z2 being Element of FS st
( FD . (x,z19) = a & FD . (z19,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )take
z29
;
( FD . (x,z19) = a & FD . (z19,z29) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z29,y) = a )A37:
dom dq1 = [:Aq1,Aq1:]
by FUNCT_2:def 1;
hence FD . (
x,
z19) =
dq1 . [x99,z1]
by A15, GRFUNC_1:2
.=
a
by A34
;
( FD . (z19,z29) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z29,y) = a )thus FD . (
z19,
z29) =
dq1 . [z1,z2]
by A15, A37, GRFUNC_1:2
.=
((FD . (x,y)) "\/" a) "/\" b
by A33, A35
;
FD . (z29,y) = athus FD . (
z29,
y) =
dq1 . [z2,y99]
by A15, A37, GRFUNC_1:2
.=
a
by A36
;
verum end;