deffunc H₁( object ) -> set = $1 `1 ;
set S = { [a,f] where a is Element of L, f is Element of F : a in f } ;
Top (BoolePoset O) = O by YELLOW_1:19;
then reconsider f = O as Element of F by WAYBEL12:8;
reconsider f = f as Subset of L ;
consider a being Element of L such that
A1: a in f by SUBSET_1:4;
reconsider a = a as Element of L ;
[a,f] in { [a,f] where a is Element of L, f is Element of F : a in f } by A1;
then reconsider S = { [a,f] where a is Element of L, f is Element of F : a in f } as non empty set ;
defpred S<sub>1</sub>[ object , object ] means $2 `2 c= $1 `2 ;
consider R being Relation of S,S such that
A2: for x, y being Element of S holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
A3: for x being object st x in S holds
H₁(x) in the carrier of L

proof

let x be object ; :: thesis: ( x in S implies H₁(x) in the carrier of L )
assume x in S ; :: thesis: H₁(x) in the carrier of L
then consider a being Element of L, f being Element of F such that
A4: x = [a,f] and
a in f ;
thus H₁(x) in the carrier of L by A4; :: thesis: verum

end;

consider h being Function of S, the carrier of L such that
A5: for x being object st x in S holds
h . x = H₁(x) from FUNCT_2:sch 2(A3);
take N = NetStr(# S,R,h #); :: thesis: ( the carrier of N = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of N holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of N holds N . i = i `1 ) )
for i, j being Element of N holds
( i <= j iff j `2 c= i `2 )

proof

let i, j be Element of N; :: thesis: ( i <= j iff j `2 c= i `2 )
reconsider x = i, y = j as Element of S ;
( [x,y] in the InternalRel of N iff y `2 c= x `2 ) by A2;
hence ( i <= j iff j `2 c= i `2 ) by ORDERS_2:def 5; :: thesis: verum

end;

hence ( the carrier of N = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of N holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of N holds N . i = i `1 ) ) by A5; :: thesis: verum