let A, B, C, p be set ; ( A /\ B c= {p} & p in C & C misses B implies A \/ C misses B )
assume that
A1:
A /\ B c= {p}
and
A2:
p in C
and
A3:
C misses B
; A \/ C misses B
{p} c= C
by A2, Lm1;
then
A /\ B c= C
by A1, XBOOLE_1:1;
then
(A /\ B) /\ B c= C /\ B
by XBOOLE_1:27;
then A4:
A /\ (B /\ B) c= C /\ B
by XBOOLE_1:16;
(A \/ C) /\ B =
(A /\ B) \/ (C /\ B)
by XBOOLE_1:23
.=
C /\ B
by A4, XBOOLE_1:12
.=
{}
by A3, XBOOLE_0:def 7
;
hence
A \/ C misses B
by XBOOLE_0:def 7; verum