:: deftheorem Def3 defines \/ XBOOLE_0:def 3 :
for X, Y, b₃ being set holds
( b₃ = X \/ Y iff for x being object holds
( x in b₃ iff ( x in X or x in Y ) ) );