let S be non empty 1-sorted ; :: thesis:
let N be net of S; :: thesis:
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:
assume A1: for A being Element of F holds A is Subset of S,N ; :: thesis:

let x be object ; :: thesis:
assume x in F ; :: thesis:
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:
thus y in the carrier of N ; :: thesis:
thus S₁[x,y] by A3; :: thesis:

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:
let x be object ; :: according to TARSKI:def 3 :: thesis:
A7: the carrier of (N | j) = { k where k is Element of N : j <= k } by WAYBEL_9:12;
assume x in C ; :: thesis:
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;

let X be set ; :: thesis:
assume A13: X in F ; :: thesis:
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:

end;