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

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

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

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

end;

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

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

proof

let x, y be Element of L; :: thesis: ( x in M & x <= y implies y in M )
assume that
A3: x in M and
A4: x <= y ; :: 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 L ;
( X is upper & x in X ) by A1, A3, A5, SETFAM_1:def 1;
hence y in Y by A4; :: thesis: verum

end;

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

end;

hence meet F is upper Subset of L by WAYBEL_0:def 20; :: thesis: verum

end;

end;