:: deftheorem defines (&) MATHMORP:def 8 :
for T being non empty RLSStruct
for X, B1, B2 being Subset of T holds X (&) (B1,B2) = X \/ (X (*) (B1,B2));