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