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 that
A1: x << z and
A2: 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 ) } ;
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

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R ) } or v in the carrier of L )
assume v in { u where u is Element of L : ex y being Element of L st
( [u,y] in R & [y,z] in R ) } ; :: thesis: v in the carrier of L
then ex u1 being Element of L st
( v = u1 & ex y being Element of L st
( [u1,y] in R & [y,z] in R ) ) ;
hence v in the carrier of L ; :: thesis: verum

end;

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

proof

let x1, y1 be Element of L; :: according to WAYBEL_0:def 19 :: thesis: ( not x1 in I or not y1 <= x1 or y1 in I )
assume that
A6: x1 in I and
A7: y1 <= x1 ; :: thesis: y1 in I
consider v1 being Element of L such that
A8: v1 = x1 and
A9: ex s1 being Element of L st
( [v1,s1] in R & [s1,z] in R ) by A6;
consider s1 being Element of L such that
A10: [v1,s1] in R and
A11: [s1,z] in R by A9;
s1 <= s1 ;
then [y1,s1] in R by A7, A8, A10, Def4;
hence y1 in I by A11; :: thesis: verum

end;

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 b₁ being Element of the carrier of L st
( b₁ in I & u1 <= b₁ & u2 <= b₁ ) )
assume that
A12: u1 in I and
A13: u2 in I ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in I & u1 <= b₁ & u2 <= b₁ )
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 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: contradiction
A24: I c= R -below z

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in I or a in R -below z )
assume a in I ; :: thesis: a in R -below z
then consider u being Element of L such that
A25: a = u and
A26: ex y2 being Element of L st
( [u,y2] in R & [y2,z] in R ) ;
consider y2 being Element of L such that
A27: [u,y2] in R and
A28: [y2,z] in R by A26;
A29: u <= y2 by A27, Def3;
z <= z ;
then [u,z] in R by A28, A29, Def4;
hence a in R -below z by A25; :: thesis: verum

end;

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; :: thesis: 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; :: thesis: verum