let L be complete LATTICE; :: thesis: 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; :: thesis: 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; :: thesis: ( [x,z] in R & x <> z implies ex y being Element of L st
( x <= y & [y,z] in R & x <> y ) )
assume A1: ( [x,z] in R & x <> z ) ; :: thesis: ex y being Element of L st
( x <= y & [y,z] in R & x <> y )
then x <= z by Def4;
then x < z by A1, ORDERS_2:def 10;
then not z < x by ORDERS_2:28;
then not z <= x by A1, ORDERS_2:def 10;
then consider u being Element of L such that
A2: ( [u,z] in R & not u <= x ) by Th49;
take y = x "\/" u; :: thesis: ( x <= y & [y,z] in R & x <> y )
thus x <= y by YELLOW_0:22; :: thesis: ( [y,z] in R & x <> y )
thus [y,z] in R by A1, A2, Def6; :: thesis: x <> y
thus x <> y by A2, YELLOW_0:24; :: thesis: verum