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

per cases ( F = {} or F <> {} ) ;

suppose A2: F = {} ; :: thesis: meet F is filtered Subset of

M is filtered

proof

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

end;

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

end;

suppose A4: F <> {} ; :: thesis: meet F is filtered Subset of

M is filtered

proof

let x, y be Element of ; :: according to WAYBEL_0:def 2 :: thesis: ( not x in M or not y in M or ex b₁ being Element of the carrier of L st
( b₁ in M & b₁ <= x & b₁ <= y ) )
assume that
A5: x in M and
A6: y in M ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in M & b₁ <= x & b₁ <= y )
take z = x "/\" y; :: thesis: ( z in M & z <= x & z <= y )
for Y being set st Y in F holds
z in Y

proof

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

end;

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

end;

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

end;

end;