let L be complete LATTICE; :: thesis: 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; :: thesis: 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; :: thesis: ( x << z & x <> z implies ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y ) )
assume A1:
( x << z & x <> z )
; :: thesis: 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 ) } ;
A2:
[(Bottom L),(Bottom L)] in R
by Def7;
[(Bottom L),z] in R
by Def7;
then A3:
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 A2;
{ 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 A3;
A4:
I is lower
I is directed
proof
let u1,
u2 be
Element of
L;
:: according to WAYBEL_0:def 1 :: thesis: ( 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 A8:
(
u1 in I &
u2 in I )
;
:: thesis: ex b1 being Element of the carrier of L st
( b1 in I & u1 <= b1 & u2 <= b1 )
then consider v1 being
Element of
L such that A9:
(
v1 = u1 & ex
y1 being
Element of
L st
(
[v1,y1] in R &
[y1,z] in R ) )
;
consider v2 being
Element of
L such that A10:
(
v2 = u2 & ex
y2 being
Element of
L st
(
[v2,y2] in R &
[y2,z] in R ) )
by A8;
consider y1 being
Element of
L such that A11:
(
[v1,y1] in R &
[y1,z] in R )
by A9;
consider y2 being
Element of
L such that A12:
(
[v2,y2] in R &
[y2,z] in R )
by A10;
take
u1 "\/" u2
;
:: thesis: ( u1 "\/" u2 in I & u1 <= u1 "\/" u2 & u2 <= u1 "\/" u2 )
A13:
[(u1 "\/" u2),(y1 "\/" y2)] in R
by A9, A10, A11, A12, Th1;
[(y1 "\/" y2),z] in R
by A11, A12, Def6;
hence
(
u1 "\/" u2 in I &
u1 <= u1 "\/" u2 &
u2 <= u1 "\/" u2 )
by A13, YELLOW_0:22;
:: thesis: verum
end;
then reconsider I = I as Ideal of L by A4;
sup I = z
proof
set z' =
sup I;
assume A14:
sup I <> z
;
:: thesis: contradiction
A15:
I c= R -below z
(
ex_sup_of I,
L &
ex_sup_of R -below z,
L )
by YELLOW_0:17;
then A19:
sup I <= sup (R -below z)
by A15, YELLOW_0:34;
z = sup (R -below z)
by Def18;
then
sup I < z
by A14, A19, ORDERS_2:def 10;
then
not
z <= sup I
by ORDERS_2:30;
then consider y being
Element of
L such that A20:
(
[y,z] in R & not
y <= sup I )
by Th49;
consider u being
Element of
L such that A21:
(
[u,y] in R & not
u <= sup I )
by A20, Th49;
A22:
u in I
by A20, A21;
(
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 A21, A22, LATTICE3:def 9, YELLOW_0:17;
:: thesis: verum
end;
then
x in I
by A1, WAYBEL_3:20;
then consider v being Element of L such that
A23:
( v = x & ex y' being Element of L st
( [v,y'] in R & [y',z] in R ) )
;
consider y' being Element of L such that
A24:
( [v,y'] in R & [y',z] in R )
by A23;
A25:
x <= y'
by A23, A24, Def4;
z <= z
;
then
[x,z] in R
by A24, A25, Def5;
then consider y'' being Element of L such that
A26:
( x <= y'' & [y'',z] in R & x <> y'' )
by A1, Th50;
A27:
x < y''
by A26, ORDERS_2:def 10;
set Y = y' "\/" y'';
A28:
( y' <= y' "\/" y'' & y'' <= y' "\/" y'' )
by YELLOW_0:22;
then A29:
x <> y' "\/" y''
by A27, ORDERS_2:32;
x <= x
;
then A30:
[x,(y' "\/" y'')] in R
by A23, A24, A28, Def5;
[(y' "\/" y''),z] in R
by A24, A26, Def6;
hence
ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
by A29, A30; :: thesis: verum