let L be antisymmetric with_infima RelStr ; :: thesis:
let F be Subset-Family of L; :: thesis:
assume A1: for X being Subset of L st X in F holds
( X is upper & X is filtered ) ; :: thesis:
reconsider F' = F as Subset-Family of L ;
reconsider M = meet F' as Subset of L ;

per cases ;

suppose A2: F = {} ; :: thesis:

M is filtered

proof

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis:
assume ( x in M & y in M ) ; :: thesis:
hence ex b₁ being Element of the carrier of L st
( b₁ in M & b₁ <= x & b₁ <= y ) by A2, SETFAM_1:def 1; :: thesis:

end;

hence meet F is filtered Subset of L ; :: thesis:

end;

suppose A3: F <> {} ; :: thesis:

M is filtered

proof

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis:
assume A4: ( x in M & y in M ) ; :: thesis:
take z = x "/\" y; :: thesis:
for Y being set st Y in F holds
z in Y

proof

let Y be set ; :: thesis:
assume A5: Y in F ; :: thesis:
then reconsider X = Y as Subset of L ;
A6: ( X is upper & X is filtered ) by A1, A5;
( x in X & y in X ) by A4, A5, SETFAM_1:def 1;
hence z in Y by A6, WAYBEL_0:41; :: thesis:

end;

hence z in M by A3, SETFAM_1:def 1; :: thesis:
thus ( z <= x & z <= y ) by YELLOW_0:23; :: thesis:

end;

hence meet F is filtered Subset of L ; :: thesis:

end;

end;