let L be Nelson_Algebra; :: thesis: for a, b, c being Element of L st a <= b & b <= c holds
a <= c
let a, b, c be Element of L; :: thesis: ( a <= b & b <= c implies a <= c )
assume ( a <= b & b <= c ) ; :: thesis: a <= c
then ( a [= b & b [= c ) by LATTICES:4;
hence a <= c by LATTICES:4, LATTICES:7; :: thesis: verum