let T be non empty 1-sorted ; :: thesis: for N being net of T holds N is subnet of N
let N be net of T; :: thesis: N is subnet of N
take id N ; :: according to YELLOW_6:def 12 :: thesis: ( the mapping of N = the mapping of N * (id N) & ( for m being Element of N ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p ) )
thus the mapping of N = the mapping of N * (id N) by TMAP_1:93; :: thesis: for m being Element of N ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p
let m be Element of N; :: thesis: ex n being Element of N st
for p being Element of N st n <= p holds
m <= (id N) . p
take n = m; :: thesis: for p being Element of N st n <= p holds
m <= (id N) . p
let p be Element of N; :: thesis: ( n <= p implies m <= (id N) . p )
assume n <= p ; :: thesis: m <= (id N) . p
hence m <= (id N) . p by TMAP_1:91; :: thesis: verum