let x be Element of L; :: thesis:
assume x in X ; :: thesis:
then consider y being Element of L such that
A2: y in X and
A3: y << x by A1;
y in { y1 where y1 is Element of L : y1 << x } by A3;
then y in waybelow x by WAYBEL_3:def 3;
hence waybelow x meets X by A2, XBOOLE_0:3; :: thesis:

end;

let x1 be Element of L; :: thesis:
assume x1 in X ; :: thesis:
then waybelow x1 meets X by A4;
then consider y being object such that
A5: y in waybelow x1 and
A6: y in X by XBOOLE_0:3;
waybelow x1 = { y1 where y1 is Element of L : y1 << x1 } by WAYBEL_3:def 3;
then ex z being Element of L st
( z = y & z << x1 ) by A5;
hence ex z being Element of L st
( z in X & z << x1 ) by A6; :: thesis:

end;