let S1, S2 be non empty 1-sorted ; :: thesis: ( the carrier of S1 = the carrier of S2 implies NetUniv S1 = NetUniv S2 )
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: NetUniv S1 = NetUniv S2

A2: now :: thesis: for x being object holds
( ( x in NetUniv S1 implies S₁[x] ) & ( S₁[x] implies x in NetUniv S1 ) )

let x be object ; :: thesis: ( ( x in NetUniv S1 implies S₁[x] ) & ( S₁[x] implies x in NetUniv S1 ) )

hereby :: thesis: ( S₁[x] implies x in NetUniv S1 )

assume x in NetUniv S1 ; :: thesis: S₁[x]
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: verum

proof

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

end;

end;

assume S₁[x] ; :: thesis: x in NetUniv S1
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: ex N being strict net of S1 st
( N = x & the carrier of N in the_universe_of the carrier of S1 )

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

end;

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

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: verum