let L be lower-bounded LATTICE; :: thesis: for S being ExtensionSeq 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, z3 being Element of FS st
( FD . x,z1 = a & FD . z2,z3 = a & FD . z1,z2 = b & FD . z3,y = b )
let S be ExtensionSeq of the carrier of L, BasicDF L; :: thesis: 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, z3 being Element of FS st
( FD . x,z1 = a & FD . z2,z3 = a & FD . z1,z2 = b & FD . z3,y = b )
let FS be non empty set ; :: thesis: 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, z3 being Element of FS st
( FD . x,z1 = a & FD . z2,z3 = a & FD . z1,z2 = b & FD . z3,y = b )
let FD be distance_function of FS,L; :: thesis: 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, z3 being Element of FS st
( FD . x,z1 = a & FD . z2,z3 = a & FD . z1,z2 = b & FD . z3,y = b )
let x, y be Element of FS; :: thesis: 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, z3 being Element of FS st
( FD . x,z1 = a & FD . z2,z3 = a & FD . z1,z2 = b & FD . z3,y = b )
let a, b be Element of L; :: thesis: ( 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, z3 being Element of FS st
( FD . x,z1 = a & FD . z2,z3 = a & FD . z1,z2 = b & FD . z3,y = b ) )
assume that
A1:
( FS = union { ((S . i) `1 ) where i is Element of NAT : verum } & FD = union { ((S . i) `2 ) where i is Element of NAT : verum } )
and
A2:
FD . x,y <= a "\/" b
; :: thesis: ex z1, z2, z3 being Element of FS st
( FD . x,z1 = a & FD . z2,z3 = a & FD . z1,z2 = b & FD . z3,y = b )
(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
A3:
( x in x1 & x1 in X )
by A1, TARSKI:def 4;
consider k being Element of NAT such that
A4:
x1 = (S . k) `1
by A3;
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
A5:
Aq1,dq1 is_extension_of A1,d1
and
A6:
( S . k = [A1,d1] & S . (k + 1) = [Aq1,dq1] )
by Def21;
A7:
(S . k) `2 = d1
by A6, MCART_1:def 2;
A8:
(S . k) `1 = A1
by A6, MCART_1:def 1;
A9:
(S . (k + 1)) `1 = Aq1
by A6, MCART_1:def 1;
A10:
(S . (k + 1)) `2 = dq1
by A6, MCART_1:def 2;
d1 in { ((S . i) `2 ) where i is Element of NAT : verum }
by A7;
then A11:
d1 c= FD
by A1, ZFMISC_1:92;
dq1 in { ((S . i) `2 ) where i is Element of NAT : verum }
by A10;
then A12:
dq1 c= FD
by A1, ZFMISC_1:92;
Aq1 in { ((S . i) `1 ) where i is Element of NAT : verum }
by A9;
then A13:
Aq1 c= FS
by A1, ZFMISC_1:92;
A14:
x in A1
by A3, A4, A6, MCART_1:def 1;
consider y1 being set such that
A15:
( y in y1 & y1 in X )
by A1, TARSKI:def 4;
consider l being Element of NAT such that
A16:
y1 = (S . l) `1
by A15;
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
A17:
Aq2,dq2 is_extension_of A2,d2
and
A18:
( S . l = [A2,d2] & S . (l + 1) = [Aq2,dq2] )
by Def21;
A19:
(S . l) `2 = d2
by A18, MCART_1:def 2;
A20:
(S . l) `1 = A2
by A18, MCART_1:def 1;
A21:
(S . (l + 1)) `1 = Aq2
by A18, MCART_1:def 1;
A22:
(S . (l + 1)) `2 = dq2
by A18, MCART_1:def 2;
d2 in { ((S . i) `2 ) where i is Element of NAT : verum }
by A19;
then A23:
d2 c= FD
by A1, ZFMISC_1:92;
dq2 in { ((S . i) `2 ) where i is Element of NAT : verum }
by A22;
then A24:
dq2 c= FD
by A1, ZFMISC_1:92;
Aq2 in { ((S . i) `1 ) where i is Element of NAT : verum }
by A21;
then A25:
Aq2 c= FS
by A1, ZFMISC_1:92;
A26:
y in A2
by A15, A16, A18, MCART_1:def 1;
per cases
( k <= l or l <= k )
;
suppose
k <= l
;
:: thesis: ex z1, z2, z3 being Element of FS st
( FD . x,z1 = a & FD . z2,z3 = a & FD . z1,z2 = b & FD . z3,y = b )then
A1 c= A2
by A8, A20, Th41;
then reconsider x' =
x,
y' =
y as
Element of
A2 by A14, A15, A16, A18, MCART_1:def 1;
A27:
(
x' in A2 &
y' in A2 )
;
dom d2 = [:A2,A2:]
by FUNCT_2:def 1;
then FD . x,
y =
d2 . [x',y']
by A23, GRFUNC_1:8
.=
d2 . x',
y'
;
then consider z1,
z2,
z3 being
Element of
Aq2 such that A28:
dq2 . x,
z1 = a
and A29:
dq2 . z2,
z3 = a
and A30:
dq2 . z1,
z2 = b
and A31:
dq2 . z3,
y = b
by A2, A17, Th40;
(
z1 in Aq2 &
z2 in Aq2 &
z3 in Aq2 )
;
then reconsider z1' =
z1,
z2' =
z2,
z3' =
z3 as
Element of
FS by A25;
A2 c= Aq2
by A20, A21, Th41, NAT_1:11;
then reconsider x'' =
x',
y'' =
y' as
Element of
Aq2 by A27;
A32:
dom dq2 = [:Aq2,Aq2:]
by FUNCT_2:def 1;
take
z1'
;
:: thesis: ex z2, z3 being Element of FS st
( FD . x,z1' = a & FD . z2,z3 = a & FD . z1',z2 = b & FD . z3,y = b )take
z2'
;
:: thesis: ex z3 being Element of FS st
( FD . x,z1' = a & FD . z2',z3 = a & FD . z1',z2' = b & FD . z3,y = b )take
z3'
;
:: thesis: ( FD . x,z1' = a & FD . z2',z3' = a & FD . z1',z2' = b & FD . z3',y = b )thus FD . x,
z1' =
dq2 . [x'',z1]
by A24, A32, GRFUNC_1:8
.=
a
by A28
;
:: thesis: ( FD . z2',z3' = a & FD . z1',z2' = b & FD . z3',y = b )thus FD . z2',
z3' =
dq2 . [z2,z3]
by A24, A32, GRFUNC_1:8
.=
a
by A29
;
:: thesis: ( FD . z1',z2' = b & FD . z3',y = b )thus FD . z1',
z2' =
dq2 . [z1,z2]
by A24, A32, GRFUNC_1:8
.=
b
by A30
;
:: thesis: FD . z3',y = bthus FD . z3',
y =
dq2 . [z3,y'']
by A24, A32, GRFUNC_1:8
.=
b
by A31
;
:: thesis: verum end; suppose
l <= k
;
:: thesis: ex z1, z2, z3 being Element of FS st
( FD . x,z1 = a & FD . z2,z3 = a & FD . z1,z2 = b & FD . z3,y = b )then
A2 c= A1
by A8, A20, Th41;
then reconsider x' =
x,
y' =
y as
Element of
A1 by A3, A4, A6, A26, MCART_1:def 1;
A33:
(
x' in A1 &
y' in A1 )
;
dom d1 = [:A1,A1:]
by FUNCT_2:def 1;
then FD . x,
y =
d1 . [x',y']
by A11, GRFUNC_1:8
.=
d1 . x',
y'
;
then consider z1,
z2,
z3 being
Element of
Aq1 such that A34:
dq1 . x,
z1 = a
and A35:
dq1 . z2,
z3 = a
and A36:
dq1 . z1,
z2 = b
and A37:
dq1 . z3,
y = b
by A2, A5, Th40;
(
z1 in Aq1 &
z2 in Aq1 &
z3 in Aq1 )
;
then reconsider z1' =
z1,
z2' =
z2,
z3' =
z3 as
Element of
FS by A13;
A1 c= Aq1
by A8, A9, Th41, NAT_1:11;
then reconsider x'' =
x',
y'' =
y' as
Element of
Aq1 by A33;
A38:
dom dq1 = [:Aq1,Aq1:]
by FUNCT_2:def 1;
take
z1'
;
:: thesis: ex z2, z3 being Element of FS st
( FD . x,z1' = a & FD . z2,z3 = a & FD . z1',z2 = b & FD . z3,y = b )take
z2'
;
:: thesis: ex z3 being Element of FS st
( FD . x,z1' = a & FD . z2',z3 = a & FD . z1',z2' = b & FD . z3,y = b )take
z3'
;
:: thesis: ( FD . x,z1' = a & FD . z2',z3' = a & FD . z1',z2' = b & FD . z3',y = b )thus FD . x,
z1' =
dq1 . [x'',z1]
by A12, A38, GRFUNC_1:8
.=
a
by A34
;
:: thesis: ( FD . z2',z3' = a & FD . z1',z2' = b & FD . z3',y = b )thus FD . z2',
z3' =
dq1 . [z2,z3]
by A12, A38, GRFUNC_1:8
.=
a
by A35
;
:: thesis: ( FD . z1',z2' = b & FD . z3',y = b )thus FD . z1',
z2' =
dq1 . [z1,z2]
by A12, A38, GRFUNC_1:8
.=
b
by A36
;
:: thesis: FD . z3',y = bthus FD . z3',
y =
dq1 . [z3,y'']
by A12, A38, GRFUNC_1:8
.=
b
by A37
;
:: thesis: verum end;