set A = {{}};
set B = the Element of {{}};
set C = the UnOp of {{}};
set D = the BinOp of {{}};
reconsider N = NelsonStr(# {{}}, the Element of {{}}, the UnOp of {{}}, the UnOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) as non empty NelsonStr ;
take N ; :: thesis: ( N is trivial & N is DeMorgan & N is involutive & N is bounded & N is distributive & N is Lattice-like )
A1: now :: thesis: for x, y being Element of N holds
( x = y & x = {} )
let x, y be Element of N; :: thesis: ( x = y & x = {} )
( x = {} & y = {} ) by TARSKI:def 1;
hence ( x = y & x = {} ) ; :: thesis: verum
end;
thus N is trivial ; :: thesis: ( N is DeMorgan & N is involutive & N is bounded & N is distributive & N is Lattice-like )
thus N is DeMorgan by A1; :: thesis: ( N is involutive & N is bounded & N is distributive & N is Lattice-like )
thus N is involutive by A1; :: thesis: ( N is bounded & N is distributive & N is Lattice-like )
thus ( N is bounded & N is distributive ) :: thesis: N is Lattice-like
proof
reconsider E = {} as Element of N by TARSKI:def 1;
for x being Element of N holds
( E "\/" x = E & x "\/" E = E & x "/\" E = E & E "/\" x = E ) by TARSKI:def 1;
then ( N is lower-bounded & N is upper-bounded ) ;
hence N is bounded ; :: thesis: N is distributive
let x, y, z be Element of N; :: according to LATTICES:def 11 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A1; :: thesis: verum
end;
( N is join-commutative & N is join-associative & N is meet-absorbing & N is meet-commutative & N is meet-associative & N is join-absorbing ) by A1;
hence N is Lattice-like ; :: thesis: verum