let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds (a "/\" b) => b = Top L
let a, b be Element of L; :: thesis: (a "/\" b) => b = Top L
a "/\" b < b by Th6;
hence (a "/\" b) => b = Top L ; :: thesis: verum