:: deftheorem defines are_compatible_wrt_5_locs NOMIN_6:def 13 :
for V being set
for loc being b₁ -valued Function
for val being Function holds
( loc,val are_compatible_wrt_5_locs iff ( val . 5 <> loc /. 4 & val . 5 <> loc /. 3 & val . 5 <> loc /. 2 & val . 5 <> loc /. 1 & val . 4 <> loc /. 3 & val . 4 <> loc /. 2 & val . 4 <> loc /. 1 & val . 3 <> loc /. 2 & val . 3 <> loc /. 1 & val . 2 <> loc /. 1 ) );