assume not X is empty ; :: thesis:
then reconsider X9 = X as non empty set ;
assume A1: X is filtered ; :: thesis:
let Y be finite Subset of X; :: thesis:
defpred S₁[ set ] means ex x being Element of L st
( x in X & x is_<=_than $1 );
A2: Y is finite ;
set x = the Element of X9;
the Element of X9 in X ;
then reconsider x = the Element of X9 as Element of L ;
x is_<=_than {} ;
then A3: S₁[ {} ] ;

let x, B be set ; :: thesis:
assume that
A5: x in Y and
B c= Y ; :: thesis:
assume S₁[B] ; :: thesis:
then consider y being Element of L such that
A6: y in X and
A7: y is_<=_than B ;
x in X by A5;
then reconsider x9 = x as Element of L ;
consider z being Element of L such that
A8: z in X and
A9: x9 >= z and
A10: y >= z by A1, A5, A6;
thus S₁[B \/ {x}] :: thesis:

take z ; :: thesis:
thus z in X by A8; :: thesis:
let a be Element of L; :: according to LATTICE3:def 8 :: thesis:
reconsider a9 = a as Element of L ;
assume a in B \/ {x} ; :: thesis:
then ( a9 in B or a9 in {x} ) by XBOOLE_0:def 3;
then ( y <= a9 or a9 = x ) by A7, TARSKI:def 1;
hence z <= a by A9, A10, ORDERS_2:3; :: thesis:

end;

end;