let L be antisymmetric with_suprema RelStr ; :: thesis: for F being Subset-Family of L st ( for X being Subset of L st X in F holds
( X is lower & X is directed ) ) holds
meet F is directed Subset of L
let F be Subset-Family of L; :: thesis: ( ( for X being Subset of L st X in F holds
( X is lower & X is directed ) ) implies meet F is directed Subset of L )
assume A1: for X being Subset of L st X in F holds
( X is lower & X is directed ) ; :: thesis: meet F is directed Subset of L
reconsider F9 = F as Subset-Family of L ;
reconsider M = meet F9 as Subset of L ;

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

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

M is directed by A2, SETFAM_1:def 1;
hence meet F is directed Subset of L ; :: thesis: verum

end;

suppose A3: F <> {} ; :: thesis: meet F is directed Subset of L

M is directed

proof

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not x in M or not y in M or ex b₁ being Element of the carrier of L st
( b₁ in M & x <= b₁ & y <= b₁ ) )
assume that
A4: x in M and
A5: y in M ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in M & x <= b₁ & y <= b₁ )
take z = x "\/" y; :: thesis: ( z in M & x <= z & y <= z )
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 A6: Y in F ; :: thesis: z in Y
then reconsider X = Y as Subset of L ;
A7: y in X by A5, A6, SETFAM_1:def 1;
( X is lower & X is directed & x in X ) by A1, A4, A6, SETFAM_1:def 1;
hence z in Y by A7, WAYBEL_0:40; :: thesis: verum

end;

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

end;

hence meet F is directed Subset of L ; :: thesis: verum

end;

end;