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