environ
vocabularies HIDDEN, ORDERS_2, ARYTM_0, RELAT_1, SUBSET_1, XXREAL_0, XBOOLE_0, RELAT_2, STRUCT_0, LATTICE3, YELLOW_0, EQREL_1, LATTICES, REWRITE1, WAYBEL_0, TARSKI, FINSET_1, XXREAL_2, XBOOLEAN, FUNCT_1, CAT_1, WELLORD1, SEQM_3, WAYBEL_1, PBOOLE, WAYBEL_5, FUNCT_6, FUNCOP_1, FINSEQ_4, YELLOW_2, ORDINAL2, CARD_3, YELLOW_7, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, CARD_3, FUNCT_6, PRALG_1, PBOOLE, FUNCOP_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_1, WAYBEL_0, WAYBEL_5;
definitions TARSKI, RELAT_2, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_5, XBOOLE_0;
theorems RELAT_1, FUNCT_1, FUNCT_2, CARD_3, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_5, PBOOLE, FUNCT_6, FUNCOP_1, PRALG_2, YELLOW_5, PRALG_1, XBOOLE_0, FUNCT_5, PARTFUN1;
schemes CLASSES1, FUNCT_2;
registrations RELSET_1, FUNCOP_1, FINSET_1, CARD_3, PBOOLE, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_5, SUBSET_1, FUNCT_1;
constructors HIDDEN, DOMAIN_1, LATTICE3, PRALG_1, PRALG_2, ORDERS_3, WAYBEL_1, WAYBEL_5, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities LATTICE3, YELLOW_0, WAYBEL_0, XBOOLE_0, FUNCT_6;
expansions RELAT_2, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_1;
theorem
for
S,
T being non
empty RelStr for
f being
set holds
( (
f is
Function of
S,
T implies
f is
Function of
(S opp),
T ) & (
f is
Function of
(S opp),
T implies
f is
Function of
S,
T ) & (
f is
Function of
S,
T implies
f is
Function of
S,
(T opp) ) & (
f is
Function of
S,
(T opp) implies
f is
Function of
S,
T ) & (
f is
Function of
S,
T implies
f is
Function of
(S opp),
(T opp) ) & (
f is
Function of
(S opp),
(T opp) implies
f is
Function of
S,
T ) ) ;
theorem
for
S,
T being non
empty RelStr for
f being
set holds
( (
f is
Connection of
S,
T implies
f is
Connection of
S ~ ,
T ) & (
f is
Connection of
S ~ ,
T implies
f is
Connection of
S,
T ) & (
f is
Connection of
S,
T implies
f is
Connection of
S,
T ~ ) & (
f is
Connection of
S,
T ~ implies
f is
Connection of
S,
T ) & (
f is
Connection of
S,
T implies
f is
Connection of
S ~ ,
T ~ ) & (
f is
Connection of
S ~ ,
T ~ implies
f is
Connection of
S,
T ) )
:: for L being RelStr holds L opp is with_infima iff L is with_suprema;