reconsider X = X as Subset of L ;

A1: now

let Y be finite Subset of X; :: thesis: ( Y <> {} implies ex_inf_of Y,L )
Y c= the carrier of L by XBOOLE_1:1;
hence ( Y <> {} implies ex_inf_of Y,L ) by YELLOW_0:55; :: thesis: verum

end;

A2: now

let x be Element of L; :: thesis: ( x in fininfs X implies ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" Y,L ) )
assume x in fininfs X ; :: thesis: ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" Y,L )
then ex Y being finite Subset of X st
( x = "/\" Y,L & ex_inf_of Y,L ) ;
hence ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" Y,L ) ; :: thesis: verum

end;

now

let Y be finite Subset of X; :: thesis: ( Y <> {} implies "/\" Y,L in fininfs X )
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {} ; :: thesis: "/\" Y,L in fininfs X
then ex_inf_of Z,L by YELLOW_0:55;
hence "/\" Y,L in fininfs X ; :: thesis: verum

end;

hence fininfs X is filtered by A1, A2, Th56; :: thesis: verum