let x be set ; :: according to CLASSES1:def 1 :: thesis: for b₁ being set holds
( not x in A \/ B or not b₁ c= x or b₁ in A \/ B )
let y be set ; :: thesis: ( not x in A \/ B or not y c= x or y in A \/ B )
assume that
A1: x in A \/ B and
A2: y c= x ; :: thesis: y in A \/ B
( x in A or x in B ) by A1, XBOOLE_0:def 3;
then ( y in A or y in B ) by A2, CLASSES1:def 1;
hence y in A \/ B by XBOOLE_0:def 3; :: thesis: verum