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_{1}[ 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

A4: ( dom f = F & rng f c= the carrier of N ) and

A5: for x being object st x in F holds

S_{1}[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;

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

( $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_{1}[x,y] )

consider f being Function such that ex y being object st

( y in the carrier of N & S

let x be object ; :: thesis: ( x in F implies ex y being object st

( y in the carrier of N & S_{1}[x,y] ) )

assume x in F ; :: thesis: ex y being object st

( y in the carrier of N & S_{1}[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_{1}[x,y] )

thus y in the carrier of N ; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A3; :: thesis: verum

end;( y in the carrier of N & S

assume x in F ; :: thesis: ex y being object st

( y in the carrier of N & S

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

thus y in the carrier of N ; :: thesis: S

thus S

A4: ( dom f = F & rng f c= the carrier of N ) and

A5: for x being object st x in F holds

S

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

hence
x in meet F
by SETFAM_1:def 1; :: thesis: verumx 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;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