let S be non empty 1-sorted ; :: thesis: for e being Element of S
for x being Element of (Net-Str e) holds x = e
let e be Element of S; :: thesis: for x being Element of (Net-Str e) holds x = e
let x be Element of (Net-Str e); :: thesis: x = e
the carrier of (Net-Str e) = {e} by Def11;
hence x = e by TARSKI:def 1; :: thesis: verum