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 ( a =-> b = Top L & b =-> c = Top L ) ; :: thesis: a =-> c = Top L
then ( a "/\" b = a & b "/\" c = b ) by Def6;
then a "/\" c = a by LATTICES:def 7;
hence a =-> c = Top L by Def6; :: thesis: verum