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