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 9 :: 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 FUNCT_2:17; :: 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 ; :: thesis: verum