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