let L be Nelson_Algebra; :: thesis: for a, b being Element of L st a =-> b = Top L & b =-> a = Top L holds
a = b
let a, b be Element of L; :: thesis: ( a =-> b = Top L & b =-> a = Top L implies a = b )
assume ( a =-> b = Top L & b =-> a = Top L ) ; :: thesis: a = b
then ( a "/\" b = a & b "/\" a = b ) by Def6;
hence a = b ; :: thesis: verum