let L be Nelson_Algebra; :: thesis: for b being Element of L holds (Top L) => b = b
let b be Element of L; :: thesis: (Top L) => b = b
b "/\" (Top L) < b by Def2;
then A1: b < (Top L) => b by Def4;
- ((Top L) => b) < (Top L) "/\" (- b) by Def10;
then A2: b <= (Top L) => b by A1, Th5;
A3: (Top L) "/\" ((Top L) => b) < b by Th17;
(Top L) "/\" (- b) < - ((Top L) => b) by Def9;
then (Top L) => b <= b by Th5, A3;
hence (Top L) => b = b by A2, Th3; :: thesis: verum