let L be non empty Poset; :: thesis: for x, y, z being Element of L st x << y & y << z holds
x << z
let x, y, z be Element of L; :: thesis: ( x << y & y << z implies x << z )
assume x << y ; :: thesis: ( not y << z or x << z )
then x <= y by Th1;
hence ( not y << z or x << z ) by Th2; :: thesis: verum