:: deftheorem Def92 defines '&' GRZLOG_1:def 44 :
for x, y, b₃ being LD-EqClass holds
( b₃ = x '&' y iff ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b₃ = LD-EqClassOf (t '&' u) ) );