environ
vocabularies HIDDEN, XXREAL_0, SUBSET_1, NUMBERS, MEMBERED, XBOOLE_0, ARYTM_3, TARSKI, REAL_1, XXREAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0, XREAL_0;
definitions TARSKI, XBOOLE_0, MEMBERED;
theorems XBOOLE_0, XXREAL_0, XBOOLE_1, TARSKI, AXIOMS, XREAL_0, XREAL_1, MEMBERED, ZFMISC_1;
schemes ;
registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, MEMBERED;
constructors HIDDEN, NUMBERS, XXREAL_0, XREAL_0, MEMBERED;
requirements HIDDEN, SUBSET, BOOLE;
equalities ;
expansions XBOOLE_0, MEMBERED;
theorem
for
p,
q,
r,
s being
ExtReal st
[.r,s.[ meets [.p,q.[ holds
[.r,s.[ \/ [.p,q.[ = [.(min (r,p)),(max (s,q)).[
theorem
for
p,
q,
r,
s being
ExtReal st
].r,s.] meets ].p,q.] holds
].r,s.] \/ ].p,q.] = ].(min (r,p)),(max (s,q)).]