let L be complete LATTICE; for x, z being Element of L
for R being auxiliary approximating Relation of L st x << z & x <> z holds
ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
let x, z be Element of L; for R being auxiliary approximating Relation of L st x << z & x <> z holds
ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
let R be auxiliary approximating Relation of L; ( x << z & x <> z implies ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y ) )
assume that
A1:
x << z
and
A2:
x <> z
; ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
set I = { u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R ) } ;
A3:
[(Bottom L),(Bottom L)] in R
by Def6;
[(Bottom L),z] in R
by Def6;
then A4:
Bottom L in { u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R ) }
by A3;
{ u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R ) } c= the carrier of L
then reconsider I = { u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R ) } as non empty Subset of L by A4;
A5:
I is lower
I is directed
proof
let u1,
u2 be
Element of
L;
WAYBEL_0:def 1 ( not u1 in I or not u2 in I or ex b1 being Element of the carrier of L st
( b1 in I & u1 <= b1 & u2 <= b1 ) )
assume that A12:
u1 in I
and A13:
u2 in I
;
ex b1 being Element of the carrier of L st
( b1 in I & u1 <= b1 & u2 <= b1 )
consider v1 being
Element of
L such that A14:
v1 = u1
and A15:
ex
y1 being
Element of
L st
(
[v1,y1] in R &
[y1,z] in R )
by A12;
consider v2 being
Element of
L such that A16:
v2 = u2
and A17:
ex
y2 being
Element of
L st
(
[v2,y2] in R &
[y2,z] in R )
by A13;
consider y1 being
Element of
L such that A18:
[v1,y1] in R
and A19:
[y1,z] in R
by A15;
consider y2 being
Element of
L such that A20:
[v2,y2] in R
and A21:
[y2,z] in R
by A17;
take
u1 "\/" u2
;
( u1 "\/" u2 in I & u1 <= u1 "\/" u2 & u2 <= u1 "\/" u2 )
A22:
[(u1 "\/" u2),(y1 "\/" y2)] in R
by A14, A16, A18, A20, Th1;
[(y1 "\/" y2),z] in R
by A19, A21, Def5;
hence
(
u1 "\/" u2 in I &
u1 <= u1 "\/" u2 &
u2 <= u1 "\/" u2 )
by A22, YELLOW_0:22;
verum
end;
then reconsider I = I as Ideal of L by A5;
sup I = z
proof
set z9 =
sup I;
assume A23:
sup I <> z
;
contradiction
A24:
I c= R -below z
A30:
ex_sup_of I,
L
by YELLOW_0:17;
ex_sup_of R -below z,
L
by YELLOW_0:17;
then A31:
sup I <= sup (R -below z)
by A24, A30, YELLOW_0:34;
z = sup (R -below z)
by Def17;
then
sup I < z
by A23, A31, ORDERS_2:def 6;
then
not
z <= sup I
by ORDERS_2:6;
then consider y being
Element of
L such that A32:
[y,z] in R
and A33:
not
y <= sup I
by Th48;
consider u being
Element of
L such that A34:
[u,y] in R
and A35:
not
u <= sup I
by A33, Th48;
A36:
u in I
by A32, A34;
(
sup I = "\/" (
I,
L) &
ex_sup_of I,
L iff (
sup I is_>=_than I & ( for
b being
Element of
L st
b is_>=_than I holds
sup I <= b ) ) )
by YELLOW_0:30;
hence
contradiction
by A35, A36, YELLOW_0:17;
verum
end;
then
x in I
by A1, WAYBEL_3:20;
then consider v being Element of L such that
A37:
v = x
and
A38:
ex y9 being Element of L st
( [v,y9] in R & [y9,z] in R )
;
consider y9 being Element of L such that
A39:
[v,y9] in R
and
A40:
[y9,z] in R
by A38;
A41:
x <= y9
by A37, A39, Def3;
z <= z
;
then
[x,z] in R
by A40, A41, Def4;
then consider y99 being Element of L such that
A42:
x <= y99
and
A43:
[y99,z] in R
and
A44:
x <> y99
by A2, Th49;
A45:
x < y99
by A42, A44, ORDERS_2:def 6;
set Y = y9 "\/" y99;
A46:
y9 <= y9 "\/" y99
by YELLOW_0:22;
y99 <= y9 "\/" y99
by YELLOW_0:22;
then A47:
x <> y9 "\/" y99
by A45, ORDERS_2:7;
x <= x
;
then A48:
[x,(y9 "\/" y99)] in R
by A37, A39, A46, Def4;
[(y9 "\/" y99),z] in R
by A40, A43, Def5;
hence
ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
by A47, A48; verum