deffunc H₁( set ) -> set = { NetStr(# $1,r,f #) where r is Relation of $1,$1, f is Element of Funcs ($1, the carrier of X) : NetStr(# $1,r,f #) is net of X } ;
set I = the_universe_of the carrier of X;
consider M being ManySortedSet of the_universe_of the carrier of X such that
A1: for i being set st i in the_universe_of the carrier of X holds
M . i = H₁(i) from PBOOLE:sch 7();
take IT = Union M; :: thesis: for x being object holds
( x in IT iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) )
let x be object ; :: thesis: ( x in IT iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) )
A2: Union M = union (rng M) by CARD_3:def 4;

hereby :: thesis: ( ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) implies x in IT )

assume x in IT ; :: thesis: ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X )
then consider y being set such that
A3: x in y and
A4: y in rng M by A2, TARSKI:def 4;
consider z being object such that
A5: z in dom M and
A6: M . z = y by A4, FUNCT_1:def 3;
reconsider z = z as set by TARSKI:1;
z in the_universe_of the carrier of X by A5;
then y = { NetStr(# z,r,f #) where r is Relation of z,z, f is Element of Funcs (z, the carrier of X) : NetStr(# z,r,f #) is net of X } by A1, A6;
then consider r being Relation of z,z, f being Element of Funcs (z, the carrier of X) such that
A7: x = NetStr(# z,r,f #) and
A8: NetStr(# z,r,f #) is net of X by A3;
reconsider N = NetStr(# z,r,f #) as strict net of X by A8;
take N = N; :: thesis: ( N = x & the carrier of N in the_universe_of the carrier of X )
thus N = x by A7; :: thesis: the carrier of N in the_universe_of the carrier of X
thus the carrier of N in the_universe_of the carrier of X by A5; :: thesis: verum

end;

given N being strict net of X such that A9: N = x and
A10: the carrier of N in the_universe_of the carrier of X ; :: thesis: x in IT
set i = the carrier of N;
the carrier of N in dom M by A10, PARTFUN1:def 2;
then A11: M . the carrier of N in rng M by FUNCT_1:def 3;
A12: the mapping of N in Funcs ( the carrier of N, the carrier of X) by FUNCT_2:8;
M . the carrier of N = { NetStr(# the carrier of N,r,f #) where r is Relation of the carrier of N, the carrier of N, f is Element of Funcs ( the carrier of N, the carrier of X) : NetStr(# the carrier of N,r,f #) is net of X } by A1, A10;
then N in M . the carrier of N by A12;
hence x in IT by A2, A9, A11, TARSKI:def 4; :: thesis: verum