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 that
A1: x <= y and
A2: y <= z ; :: thesis: x <= z
A3: (Net-Str (S,f)) . x <= (Net-Str (S,f)) . y by A1, Def10;
(Net-Str (S,f)) . y <= (Net-Str (S,f)) . z by A2, Def10;
then (Net-Str (S,f)) . x <= (Net-Str (S,f)) . z by A3, YELLOW_0:def 2;
hence x <= z by Def10; :: thesis: verum