let L be complete LATTICE; :: thesis: for x, y being Element of L
for AR being approximating Relation of L st not x <= y holds
ex u being Element of L st
( [u,x] in AR & not u <= y )
let x, y be Element of L; :: thesis: for AR being approximating Relation of L st not x <= y holds
ex u being Element of L st
( [u,x] in AR & not u <= y )
let AR be approximating Relation of L; :: thesis: ( not x <= y implies ex u being Element of L st
( [u,x] in AR & not u <= y ) )
assume A1: not x <= y ; :: thesis: ex u being Element of L st
( [u,x] in AR & not u <= y )
( x = sup (AR -below x) & ex_sup_of AR -below x,L ) by Def18, YELLOW_0:17;
then ( y is_>=_than AR -below x implies y >= x ) by YELLOW_0:def 9;
then consider u being Element of L such that
A2: ( u in AR -below x & not u <= y ) by A1, LATTICE3:def 9;
take u ; :: thesis: ( [u,x] in AR & not u <= y )
thus ( [u,x] in AR & not u <= y ) by A2, Th13; :: thesis: verum