let L be Nelson_Algebra; :: thesis: for a, b, c being Element of L st a => b = Top L & b => c = Top L holds
a => c = Top L
let a, b, c be Element of L; :: thesis: ( a => b = Top L & b => c = Top L implies a => c = Top L )
assume A1: ( a => b = Top L & b => c = Top L ) ; :: thesis: a => c = Top L
A2: a < b by A1;
A3: b < c by A1;
a < c by Def3, A2, A3;
hence a => c = Top L ; :: thesis: verum