deffunc H_{1}( 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_{1}[ 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_{1}[x,y] )
from RELSET_1:sch 2();

A3: for x being object st x in S holds

H_{1}(x) in the carrier of L

A5: for x being object st x in S holds

h . x = H_{1}(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 )

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of N holds N . i = i `1 ) ) by A5; :: thesis: verum

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

consider R being Relation of S,S such that

A2: for x, y being Element of S holds

( [x,y] in R iff S

A3: for x being object st x in S holds

H

proof

consider h being Function of S, the carrier of L such that
let x be object ; :: thesis: ( x in S implies H_{1}(x) in the carrier of L )

assume x in S ; :: thesis: H_{1}(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_{1}(x) in the carrier of L
by A4; :: thesis: verum

end;assume x in S ; :: thesis: H

then consider a being Element of L, f being Element of F such that

A4: x = [a,f] and

a in f ;

thus H

A5: for x being object st x in S holds

h . x = H

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

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
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;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

( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of N holds N . i = i `1 ) ) by A5; :: thesis: verum