environ
vocabularies HIDDEN, NUMBERS, LATTICES, LATTICE3, SUBSET_1, FILTER_1, PBOOLE, EQREL_1, ZFMISC_1, ROBBINS3, XBOOLE_0, ROBBINS1, OPOSET_1, ORDERS_2, YELLOW_1, CARD_1, RELAT_2, TARSKI, STRUCT_0, XXREAL_0, FILTER_0, FUNCT_1, BINOP_1, RVSUM_1, SYMSP_1, ROBBINS4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, SUBSET_1, BINOP_1, FUNCT_1, ORDINAL1, CARD_1, NUMBERS, FUNCT_2, STRUCT_0, LATTICE3, LATTICES, ORDERS_2, ROBBINS1, YELLOW_1, ROBBINS3;
definitions LATTICES, TARSKI, ROBBINS3, ROBBINS1, LATTICE3;
theorems ZFMISC_1, STRUCT_0, LATTICE3, FILTER_1, LATTICES, FUNCT_2, ROBBINS3, ROBBINS1, FILTER_0, YELLOW11, XBOOLE_1, TARSKI, ENUMSET1, XBOOLE_0, SUBSET_1, YELLOW_1, CARD_1, NAT_1, RELSET_1, YELLOW_0;
schemes FUNCT_2;
registrations SUBSET_1, RELAT_1, STRUCT_0, LATTICES, YELLOW_1, ROBBINS1, SHEFFER1, ROBBINS3, XBOOLE_0, ORDINAL1;
constructors HIDDEN, BINOP_1, REALSET2, LATTICE3, ROBBINS3, YELLOW_1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, REAL;
equalities LATTICES, ROBBINS1, SUBSET_1, LATTICE3, ORDINAL1, CARD_1;
expansions LATTICES, TARSKI, ROBBINS3, ROBBINS1;
Lm1:
3 \ 2 misses 2
by XBOOLE_1:79;
Lm2:
Segm 1 c= Segm 2
by NAT_1:39;
then Lm3:
3 \ 2 misses 1
by Lm1, XBOOLE_1:63;
theorem Th23:
for
a being
Element of
Benzene holds
( (
a = 0 implies
a ` = 3 ) & (
a = 3 implies
a ` = 0 ) & (
a = 1 implies
a ` = 3
\ 1 ) & (
a = 3
\ 1 implies
a ` = 1 ) & (
a = 2 implies
a ` = 3
\ 2 ) & (
a = 3
\ 2 implies
a ` = 2 ) )