let S1, S2 be non empty 1-sorted ; :: thesis:
defpred S₁[ object ] means ex N being strict net of S2 st
( N = $1 & the carrier of N in the_universe_of the carrier of S2 );
assume A1: the carrier of S1 = the carrier of S2 ; :: thesis:

A2: now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in NetUniv S1 ; :: thesis:
then consider N being strict net of S1 such that
A3: ( N = x & the carrier of N in the_universe_of the carrier of S1 ) by Def11;
reconsider N = N as strict net of S2 by A1;
thus S₁[x] :: thesis:

proof

take N ; :: thesis:
thus ( N = x & the carrier of N in the_universe_of the carrier of S2 ) by A1, A3; :: thesis:

end;

end;

assume S₁[x] ; :: thesis:
then consider N being strict net of S2 such that
A4: ( N = x & the carrier of N in the_universe_of the carrier of S2 ) ;
reconsider N = N as strict net of S1 by A1;

now :: thesis:

take N = N; :: thesis:
thus ( N = x & the carrier of N in the_universe_of the carrier of S1 ) by A1, A4; :: thesis:

end;

hence x in NetUniv S1 by Def11; :: thesis:

end;

A5: for x being object holds
( x in NetUniv S2 iff S₁[x] ) by Def11;
thus NetUniv S1 = NetUniv S2 from XBOOLE_0:sch 2(A2, A5); :: thesis: