let L be LATTICE; :: thesis: IntRel L is approximating
set AR = IntRel L;
let x be Element of L; :: according to WAYBEL_4:def 17 :: thesis: x = sup ((IntRel L) -below x)
set A = { y where y is Element of L : [y,x] in IntRel L } ;
set E = { u where u is Element of L : u <= x } ;
A1: { y where y is Element of L : [y,x] in IntRel L } c= { u where u is Element of L : u <= x }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of L : [y,x] in IntRel L } or a in { u where u is Element of L : u <= x } )
assume a in { y where y is Element of L : [y,x] in IntRel L } ; :: thesis: a in { u where u is Element of L : u <= x }
then consider v being Element of L such that
A2: a = v and
A3: [v,x] in IntRel L ;
v <= x by A3, ORDERS_2:def 5;
hence a in { u where u is Element of L : u <= x } by A2; :: thesis: verum

end;

{ u where u is Element of L : u <= x } c= { y where y is Element of L : [y,x] in IntRel L }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { u where u is Element of L : u <= x } or a in { y where y is Element of L : [y,x] in IntRel L } )
assume a in { u where u is Element of L : u <= x } ; :: thesis: a in { y where y is Element of L : [y,x] in IntRel L }
then consider v being Element of L such that
A4: a = v and
A5: v <= x ;
[v,x] in IntRel L by A5, ORDERS_2:def 5;
hence a in { y where y is Element of L : [y,x] in IntRel L } by A4; :: thesis: verum

end;

then A6: { y where y is Element of L : [y,x] in IntRel L } = { u where u is Element of L : u <= x } by A1;
{ y where y is Element of L : y <= x } c= the carrier of L

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Element of L : y <= x } or z in the carrier of L )
assume z in { y where y is Element of L : y <= x } ; :: thesis: z in the carrier of L
then ex y being Element of L st
( z = y & y <= x ) ;
hence z in the carrier of L ; :: thesis: verum

end;

then reconsider E = { u where u is Element of L : u <= x } as Subset of L ;
A7: x is_>=_than E

proof

let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in E or b <= x )
assume b in E ; :: thesis: b <= x
then ex b9 being Element of L st
( b9 = b & b9 <= x ) ;
hence b <= x ; :: thesis: verum

end;

now :: thesis: for b being Element of L st b is_>=_than E holds
x <= b

let b be Element of L; :: thesis: ( b is_>=_than E implies x <= b )
assume A8: b is_>=_than E ; :: thesis: x <= b
x in E ;
hence x <= b by A8; :: thesis: verum

end;

hence x = sup ((IntRel L) -below x) by A6, A7, YELLOW_0:30; :: thesis: verum