let L be complete LATTICE; for x, z being Element of L
for R being auxiliary(i) auxiliary(iii) approximating Relation of L st [x,z] in R & x <> z holds
ex y being Element of L st
( x <= y & [y,z] in R & x <> y )
let x, z be Element of L; for R being auxiliary(i) auxiliary(iii) approximating Relation of L st [x,z] in R & x <> z holds
ex y being Element of L st
( x <= y & [y,z] in R & x <> y )
let R be auxiliary(i) auxiliary(iii) approximating Relation of L; ( [x,z] in R & x <> z implies ex y being Element of L st
( x <= y & [y,z] in R & x <> y ) )
assume that
A1:
[x,z] in R
and
A2:
x <> z
; ex y being Element of L st
( x <= y & [y,z] in R & x <> y )
x <= z
by A1, Def3;
then
x < z
by A2, ORDERS_2:def 6;
then
not z < x
by ORDERS_2:4;
then
not z <= x
by A2, ORDERS_2:def 6;
then consider u being Element of L such that
A3:
[u,z] in R
and
A4:
not u <= x
by Th48;
take y = x "\/" u; ( x <= y & [y,z] in R & x <> y )
thus
x <= y
by YELLOW_0:22; ( [y,z] in R & x <> y )
thus
[y,z] in R
by A1, A3, Def5; x <> y
thus
x <> y
by A4, YELLOW_0:24; verum