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 )
A2: x = sup (AR -below x) by Def17;
ex_sup_of AR -below x,L by YELLOW_0:17;
then ( y is_>=_than AR -below x implies y >= x ) by A2, YELLOW_0:def 9;
then consider u being Element of L such that
A3: u in AR -below x and
A4: not u <= y by A1;
take u ; :: thesis: ( [u,x] in AR & not u <= y )
thus ( [u,x] in AR & not u <= y ) by A3, A4, Th13; :: thesis: verum