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
A3: x in A /\ B and
A4: y c= x ; :: thesis: y in A /\ B
x in B by A3, XBOOLE_0:def 4;
then A5: y in B by A4, CLASSES1:def 1;
x in A by A3, XBOOLE_0:def 4;
then y in A by A4, CLASSES1:def 1;
hence y in A /\ B by A5, XBOOLE_0:def 4; :: thesis: verum