environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, SUBSET_1, SETFAM_1, RCOMP_1, TARSKI, ZFMISC_1, STRUCT_0, BINOP_1, FUNCT_1, LATTICES, EQREL_1, XXREAL_2, CARD_FIL, RELAT_1, INT_2, FINSUB_1, SETWISEO, FILTER_0, LATTICE2, PBOOLE, FINSET_1, CLASSES1, CARD_1, GROUP_6, FUNCT_2, WELLORD1, LOPCLSET;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, PRE_TOPC, LATTICES, LATTICE2, FILTER_0, FINSET_1, SETWISEO, LATTICE4, CLASSES1, CARD_1;
definitions TARSKI, LATTICES, BINOP_1, STRUCT_0, XBOOLE_0;
theorems TARSKI, SETFAM_1, LATTICES, FINSUB_1, TOPS_1, PRE_TOPC, SUBSET_1, LATTICE2, LATTICE4, FILTER_0, FUNCT_1, FUNCT_2, ZFMISC_1, GROUP_6, SETWISEO, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, STRUCT_0, CLASSES1, EQREL_1;
schemes BINOP_1, FRAENKEL, FUNCT_1, SETWISEO, BINOP_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, FINSUB_1, STRUCT_0, LATTICES, PRE_TOPC, CARD_1, RELSET_1, TOPS_1, LATTICE2;
constructors HIDDEN, BINOP_1, SETWISEO, PRE_TOPC, LATTICE2, FILTER_1, CLASSES1, LATTICE4, RELSET_1, FILTER_0;
requirements HIDDEN, BOOLE, SUBSET;
equalities LATTICES, STRUCT_0, SUBSET_1;
expansions TARSKI, LATTICES, XBOOLE_0;
definition
let T be non
empty TopSpace;
deffunc H1(
Element of
OpenClosedSet T,
Element of
OpenClosedSet T)
-> Element of
OpenClosedSet T = $1
\/ $2;
existence
ex b1 being BinOp of (OpenClosedSet T) st
for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A \/ B
uniqueness
for b1, b2 being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A \/ B ) & ( for A, B being Element of OpenClosedSet T holds b2 . (A,B) = A \/ B ) holds
b1 = b2
deffunc H2(
Element of
OpenClosedSet T,
Element of
OpenClosedSet T)
-> Element of
OpenClosedSet T = $1
/\ $2;
existence
ex b1 being BinOp of (OpenClosedSet T) st
for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A /\ B
uniqueness
for b1, b2 being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A /\ B ) & ( for A, B being Element of OpenClosedSet T holds b2 . (A,B) = A /\ B ) holds
b1 = b2
end;
Lm1:
for BL being non trivial B_Lattice
for p being Subset of (StoneSpace BL) st p in StoneR BL holds
p is open
Lm2:
for BL being non trivial B_Lattice holds StoneR BL c= OpenClosedSet (StoneSpace BL)