environ
vocabularies HIDDEN, LATTICE2, FILTER_0, LATTICES, PRE_TOPC, SUBSET_1, XBOOLE_0, TOPS_1, TARSKI, RCOMP_1, SETFAM_1, BINOP_1, FUNCT_1, EQREL_1, STRUCT_0, PBOOLE, CARD_FIL, INT_2, RELAT_1, ZFMISC_1, ORDINAL1, GROUP_6, FUNCT_2, WELLORD1, XBOOLEAN, LATTICE4, OPENLATT;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, LATTICES, LATTICE2, FILTER_0, LATTICE4;
definitions TARSKI, PRE_TOPC, FILTER_0, LATTICES, LATTICE4, FUNCT_1, STRUCT_0, XBOOLE_0, FUNCT_2;
theorems PRE_TOPC, LATTICES, TOPS_1, ZFMISC_1, FILTER_0, SETFAM_1, TARSKI, FUNCT_1, FUNCT_2, LATTICE4, RELAT_1, ORDINAL1, XBOOLE_0, XBOOLE_1, STRUCT_0, EQREL_1;
schemes BINOP_1, DOMAIN_1, FUNCT_1, BINOP_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, PRE_TOPC, FILTER_0, LATTICE2, TOPS_1;
constructors HIDDEN, BINOP_1, DOMAIN_1, TOPS_1, LATTICE2, FILTER_1, LATTICE4, RELSET_1, FILTER_0;
requirements HIDDEN, BOOLE, SUBSET;
equalities FILTER_0, LATTICES, STRUCT_0, SUBSET_1;
expansions TARSKI, PRE_TOPC, FILTER_0, LATTICES, LATTICE4, FUNCT_1, XBOOLE_0, FUNCT_2;
definition
let T be non
empty TopSpace;
existence
ex b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . (P,Q) = P \/ Q
uniqueness
for b1, b2 being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b1 . (P,Q) = P \/ Q ) & ( for P, Q being Element of Topology_of T holds b2 . (P,Q) = P \/ Q ) holds
b1 = b2
existence
ex b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . (P,Q) = P /\ Q
uniqueness
for b1, b2 being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b1 . (P,Q) = P /\ Q ) & ( for P, Q being Element of Topology_of T holds b2 . (P,Q) = P /\ Q ) holds
b1 = b2
end;
Lm1:
for L being D_Lattice
for F being Filter of L
for a, b being Element of L holds
( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
definition
let L be
D_Lattice;
existence
ex b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . (A,B) = A \/ B
uniqueness
for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . (A,B) = A \/ B ) & ( for A, B being Element of StoneS L holds b2 . (A,B) = A \/ B ) holds
b1 = b2
existence
ex b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . (A,B) = A /\ B
uniqueness
for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . (A,B) = A /\ B ) & ( for A, B being Element of StoneS L holds b2 . (A,B) = A /\ B ) holds
b1 = b2
end;