environ
vocabularies HIDDEN, XBOOLE_0, LATTICES, ORDERS_2, ZFMISC_1, STRUCT_0, TARSKI, SUBSET_1, LATTICE3, RELAT_2, XXREAL_0, YELLOW_0, REWRITE1, ORDINAL2, RELAT_1, MCART_1, EQREL_1, XXREAL_2, WAYBEL_0, WAYBEL_3, RCOMP_1, WAYBEL_8, WAYBEL_6, CARD_FIL, WAYBEL11, WAYBEL_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, DOMAIN_1, STRUCT_0, MCART_1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_6, WAYBEL_8, WAYBEL11;
definitions TARSKI, YELLOW_0, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_6, WAYBEL_8, WAYBEL11, XBOOLE_0;
theorems ZFMISC_1, TARSKI, ORDERS_2, YELLOW_0, YELLOW_3, YELLOW_4, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_8, MCART_1, FUNCT_5, DOMAIN_1, XBOOLE_0, XTUPLE_0;
schemes ;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_8, WAYBEL14, RELAT_1, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, WAYBEL_1, YELLOW_4, WAYBEL_3, WAYBEL_6, WAYBEL_8, WAYBEL11, WAYBEL_2, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities YELLOW_0, WAYBEL_3, WAYBEL_8;
expansions YELLOW_0, LATTICE3, WAYBEL_1, WAYBEL_3, WAYBEL_8;
theorem
for
S,
T being non
empty antisymmetric RelStr for
x,
y being
Element of
[:S,T:] holds
(
ex_inf_of {x,y},
[:S,T:] iff (
ex_inf_of {(x `1),(y `1)},
S &
ex_inf_of {(x `2),(y `2)},
T ) )
theorem
for
S,
T being non
empty antisymmetric RelStr for
x,
y being
Element of
[:S,T:] holds
(
ex_sup_of {x,y},
[:S,T:] iff (
ex_sup_of {(x `1),(y `1)},
S &
ex_sup_of {(x `2),(y `2)},
T ) )