begin
begin
begin
begin
Lm1:
for N being non empty RelStr holds
( N is directed iff RelStr(# the carrier of N, the InternalRel of N #) is directed )
Lm2:
for N being non empty RelStr holds
( N is transitive iff RelStr(# the carrier of N, the InternalRel of N #) is transitive )
Lm3:
for R, S being RelStr
for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
begin
Lm4:
for S being 1-sorted
for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is SubNetStr of R
Lm5:
for S being 1-sorted
for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is full SubRelStr of R
begin
begin
begin
Lm6:
for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
for N being constant net of S1 holds N is constant net of S2
Lm7:
for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
NetUniv S1 = NetUniv S2
begin
definition
let T be non
empty 1-sorted ;
let Y be
net of
T;
let J be
net_set of the
carrier of
Y,
T;
existence
ex b1 being strict net of T st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b1 . (i,f) = the mapping of (J . i) . (f . i) ) )
uniqueness
for b1, b2 being strict net of T st RelStr(# the carrier of b1, the InternalRel of b1 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b1 . (i,f) = the mapping of (J . i) . (f . i) ) & RelStr(# the carrier of b2, the InternalRel of b2 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b2 . (i,f) = the mapping of (J . i) . (f . i) ) holds
b1 = b2
end;
begin
begin
begin