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