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

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

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

then for x, y being Element of st x in M & y <= x holds
y in M by SETFAM_1:def 1;
hence meet F is lower Subset of by WAYBEL_0:def 19; :: thesis: verum

end;

suppose A2: F <> {} ; :: thesis: meet F is lower Subset of

for x, y being Element of st x in M & y <= x holds
y in M

proof

let x, y be Element of ; :: thesis: ( x in M & y <= x implies y in M )
assume that
A3: x in M and
A4: y <= x ; :: thesis: y in M
for Y being set st Y in F holds
y in Y

proof

let Y be set ; :: thesis: ( Y in F implies y in Y )
assume A5: Y in F ; :: thesis: y in Y
then reconsider X = Y as Subset of ;
( X is lower & x in X ) by A1, A3, A5, SETFAM_1:def 1;
hence y in Y by A4, WAYBEL_0:def 19; :: thesis: verum

end;

hence y in M by A2, SETFAM_1:def 1; :: thesis: verum

end;

hence meet F is lower Subset of by WAYBEL_0:def 19; :: thesis: verum

end;

end;