let L be LATTICE; :: thesis: IntRel L is approximating
set AR = IntRel L;
let x be Element of L; :: according to WAYBEL_4:def 18 :: 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 } = { u where u is Element of L : u <= x }

proof

thus { y where y is Element of L : [y,x] in IntRel L } c= { u where u is Element of L : u <= x } :: according to XBOOLE_0:def 10 :: thesis: { 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 set ; :: 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 9;
hence a in { u where u is Element of L : u <= x } by A2; :: thesis: verum

end;

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

proof

let a be set ; :: 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 9;
hence a in { y where y is Element of L : [y,x] in IntRel L } by A4; :: thesis: verum

end;

end;

{ y where y is Element of L : y <= x } c= the carrier of L

proof

let z be set ; :: 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 ;
A6: 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 consider b' being Element of L such that
A7: ( b' = b & b' <= x ) ;
thus b <= x by A7; :: thesis: verum

end;

now

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, LATTICE3:def 9; :: thesis: verum

end;

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