:: deftheorem Def3 defines divset SURREALI:def 3 :
for Lamb being set
for x being object
for X being set
for Inv being Function
for b₅ being set holds
( b₅ = divset (Lamb,x,X,Inv) iff for o being object holds
( o in b₅ iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) ) );