let S be non empty reflexive RelStr ; :: thesis: for e being Element of S holds Net-Str e in NetUniv S
let e be Element of S; :: thesis: Net-Str e in NetUniv S
set N = Net-Str e;
set UN = the_universe_of the carrier of S;
A1: the carrier of (Net-Str e) = {e} by Def11;
reconsider UN = the_universe_of the carrier of S as universal set ;
the_transitive-closure_of the carrier of S in UN by CLASSES1:2;
then the carrier of S in UN by CLASSES1:3, CLASSES1:52;
then the carrier of (Net-Str e) in the_universe_of the carrier of S by A1, CLASSES1:def 1;
hence Net-Str e in NetUniv S by YELLOW_6:def 11; :: thesis: verum