begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
begin
theorem Th14:
:: deftheorem Def1 defines connected JCT_MISC:def 1 :
theorem
definition
let A,
B be
Subset of
REAL ;
func dist A,
B -> real number means :
Def2:
ex
X being
Subset of
REAL st
(
X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } &
it = lower_bound X );
existence
ex b1 being real number ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X )
uniqueness
for b1, b2 being real number st ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X ) & ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b2 = lower_bound X ) holds
b1 = b2
;
commutativity
for b1 being real number
for A, B being Subset of REAL st ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X ) holds
ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & b1 = lower_bound X )
end;
:: deftheorem Def2 defines dist JCT_MISC:def 2 :
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem