let x be Element of (Net-Str S,f); :: according to YELLOW_0:def 1 :: thesis: x <= x
(Net-Str S,f) . x <= (Net-Str S,f) . x ;
hence x <= x by Def10; :: thesis: verum