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

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

let x be set ; :: 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 and
A4: the carrier of N in the_universe_of the carrier of S1 by YELLOW_6:def 11;
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, A4; :: thesis: verum

end;

end;

assume S₂[x] ; :: thesis: x in NetUniv S1
then consider N being strict net of S2 such that
A5: N = x and
A6: 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, A5, A6; :: thesis: verum

end;

hence x in NetUniv S1 by YELLOW_6:def 11; :: thesis: verum

end;

A7: for x being set holds
( x in NetUniv S2 iff S₂[x] ) by YELLOW_6:def 11;
thus NetUniv S1 = NetUniv S2 from XFAMILY:sch 2(A2, A7); :: thesis: verum