let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds
( a "/\" b = Top L iff ( a = Top L & b = Top L ) )
let a, b be Element of L; :: thesis: ( a "/\" b = Top L iff ( a = Top L & b = Top L ) )
hereby :: thesis: ( a = Top L & b = Top L implies a "/\" b = Top L )
assume A1: a "/\" b = Top L ; :: thesis: ( a = Top L & b = Top L )
then Top L [= a by LATTICES:6;
hence a = Top L ; :: thesis: b = Top L
Top L [= b by A1, LATTICES:6;
hence b = Top L ; :: thesis: verum
end;
thus ( a = Top L & b = Top L implies a "/\" b = Top L ) ; :: thesis: verum