let L be LATTICE; :: thesis:
set AR = IntRel L;
let x be Element of L; :: according to WAYBEL_4:def 17 :: thesis:
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 }

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { y where y is Element of L : [y,x] in IntRel L } ; :: thesis:
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:

end;

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

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { u where u is Element of L : u <= x } ; :: thesis:
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:

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

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

end;

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

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

end;

end;