let S be non empty 1-sorted ; :: thesis: for N being net of S
for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds
ex B being Subset of S,N st B c= meet F
let N be net of S; :: thesis: for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds
ex B being Subset of S,N st B c= meet F
defpred S₁[ object , object ] means ex i being Element of N st
( $2 = i & $1 = rng the mapping of (N | i) );
let F be non empty finite set ; :: thesis: ( ( for A being Element of F holds A is Subset of S,N ) implies ex B being Subset of S,N st B c= meet F )
assume A1: for A being Element of F holds A is Subset of S,N ; :: thesis: ex B being Subset of S,N st B c= meet F

A2: now :: thesis: for x being object st x in F holds
ex y being object st
( y in the carrier of N & S₁[x,y] )

let x be object ; :: thesis: ( x in F implies ex y being object st
( y in the carrier of N & S₁[x,y] ) )
assume x in F ; :: thesis: ex y being object st
( y in the carrier of N & S₁[x,y] )
then reconsider A = x as Subset of S,N by A1;
consider i being Element of N such that
A3: A = rng the mapping of (N | i) by Def2;
reconsider y = i as object ;
take y = y; :: thesis: ( y in the carrier of N & S₁[x,y] )
thus y in the carrier of N ; :: thesis: S₁[x,y]
thus S₁[x,y] by A3; :: thesis: verum

end;

consider f being Function such that
A4: ( dom f = F & rng f c= the carrier of N ) and
A5: for x being object st x in F holds
S₁[x,f . x] from FUNCT_1:sch 6(A2);
reconsider B = rng f as finite Subset of N by A4, FINSET_1:8;
[#] N is directed by WAYBEL_0:def 6;
then consider j being Element of N such that
j in [#] N and
A6: j is_>=_than B by WAYBEL_0:1;
reconsider C = rng the mapping of (N | j) as Subset of S,N by Def2;
take C ; :: thesis: C c= meet F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in meet F )
A7: the carrier of (N | j) = { k where k is Element of N : j <= k } by WAYBEL_9:12;
assume x in C ; :: thesis: x in meet F
then consider y being object such that
A8: y in dom the mapping of (N | j) and
A9: x = the mapping of (N | j) . y by FUNCT_1:def 3;
A10: y in the carrier of (N | j) by A8;
reconsider y = y as Element of (N | j) by A8;
consider k being Element of N such that
A11: y = k and
A12: j <= k by A10, A7;

now :: thesis: for X being set st X in F holds
x in X

let X be set ; :: thesis: ( X in F implies x in X )
assume A13: X in F ; :: thesis: x in X
then consider i being Element of N such that
A14: f . X = i and
A15: X = rng the mapping of (N | i) by A5;
i in B by A4, A13, A14, FUNCT_1:def 3;
then i <= j by A6, LATTICE3:def 9;
then i <= k by A12, ORDERS_2:3;
then y in { l where l is Element of N : i <= l } by A11;
then reconsider z = y as Element of (N | i) by WAYBEL_9:12;
x = (N | j) . y by A9
.= N . k by A11, WAYBEL_9:16
.= (N | i) . z by A11, WAYBEL_9:16
.= the mapping of (N | i) . z ;
hence x in X by A15, FUNCT_2:4; :: thesis: verum

end;

hence x in meet F by SETFAM_1:def 1; :: thesis: verum