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 that
A1: [x,z] in R and
A2: x <> z ; :: thesis: 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; :: 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, A3, Def5; :: thesis: x <> y
thus x <> y by A4, YELLOW_0:24; :: thesis: verum