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