:: deftheorem Def5 defines symmetric LATTICE5:def 5 :
for A being non empty set
for L being 1-sorted
for f being BiFunction of A,L holds
( f is symmetric iff for x, y being Element of A holds f . (x,y) = f . (y,x) );