let n be Element of NAT ; for r being real number
for y, x, z being Point of (TOP-REAL n) st y in Sphere x,r & z in Sphere x,r holds
(LSeg y,z) /\ (Sphere x,r) = {y,z}
let r be real number ; for y, x, z being Point of (TOP-REAL n) st y in Sphere x,r & z in Sphere x,r holds
(LSeg y,z) /\ (Sphere x,r) = {y,z}
let y, x, z be Point of (TOP-REAL n); ( y in Sphere x,r & z in Sphere x,r implies (LSeg y,z) /\ (Sphere x,r) = {y,z} )
A1:
( y in LSeg y,z & z in LSeg y,z )
by RLTOPSP1:69;
assume A2:
( y in Sphere x,r & z in Sphere x,r )
; (LSeg y,z) /\ (Sphere x,r) = {y,z}
then A3:
(LSeg y,z) \ {y,z} c= Ball x,r
by Th34;
hereby TARSKI:def 3,
XBOOLE_0:def 10 {y,z} c= (LSeg y,z) /\ (Sphere x,r)
let a be
set ;
( a in (LSeg y,z) /\ (Sphere x,r) implies a in {y,z} )assume A4:
a in (LSeg y,z) /\ (Sphere x,r)
;
a in {y,z}assume A5:
not
a in {y,z}
;
contradiction
a in LSeg y,
z
by A4, XBOOLE_0:def 4;
then A6:
a in (LSeg y,z) \ {y,z}
by A5, XBOOLE_0:def 5;
A7:
Ball x,
r misses Sphere x,
r
by Th19;
a in Sphere x,
r
by A4, XBOOLE_0:def 4;
hence
contradiction
by A3, A6, A7, XBOOLE_0:3;
verum
end;
let a be set ; TARSKI:def 3 ( not a in {y,z} or a in (LSeg y,z) /\ (Sphere x,r) )
assume
a in {y,z}
; a in (LSeg y,z) /\ (Sphere x,r)
then
( a = y or a = z )
by TARSKI:def 2;
hence
a in (LSeg y,z) /\ (Sphere x,r)
by A2, A1, XBOOLE_0:def 4; verum