environ
vocabularies HIDDEN, XBOOLE_0, ORDERS_2, PARTFUN1, STRUCT_0, FINSEQ_1, RELAT_1, TARSKI, RELAT_2, SUBSET_1, XXREAL_0, LATTICE3, WAYBEL_0, EQREL_1, LATTICES;
notations HIDDEN, XBOOLE_0, TARSKI, SUBSET_1, RELSET_1, RELAT_2, STRUCT_0, ORDERS_2, YELLOW_0, WAYBEL_0, LATTICE3;
definitions RELAT_2;
theorems ZFMISC_1, RELAT_1, RELSET_1, ORDERS_2, XBOOLE_0, XBOOLE_1, WAYBEL_0, YELLOW_0, YELLOW_5;
schemes ;
registrations XBOOLE_0, RELSET_1, STRUCT_0, WAYBEL_0;
constructors HIDDEN, LATTICE3, WAYBEL_0, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities ;
expansions RELAT_2;
theorem
for
x,
y,
A,
B being
set st
x in A \/ B &
y in A \/ B & not (
x in A \ B &
y in A \ B ) & not (
x in B &
y in B ) & not (
x in A \ B &
y in B ) holds
(
x in B &
y in A \ B )