let p be object ; :: thesis: for A, B, C being set st A /\ B c= {p} & p in C & C misses B holds
A \/ C misses B
let A, B, C be set ; :: thesis: ( 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 ; :: thesis: A \/ C misses B
{p} c= C by A2, Lm1;
then A /\ B c= C by A1;
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
.= {} by A3, A4, XBOOLE_1:12 ;
hence A \/ C misses B ; :: thesis: verum