set N = Net-Str S,f;
let x, y, z be Element of (Net-Str S,f); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume ( x <= y & y <= z ) ; :: thesis: x <= z
then ( (Net-Str S,f) . x <= (Net-Str S,f) . y & (Net-Str S,f) . y <= (Net-Str S,f) . z ) by Def10;
then (Net-Str S,f) . x <= (Net-Str S,f) . z by YELLOW_0:def 2;
hence x <= z by Def10; :: thesis: verum