let n be Element of NAT ; :: thesis: 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 ; :: thesis: 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); :: thesis: ( y in Sphere x,r & z in Sphere x,r implies (LSeg y,z) /\ (Sphere x,r) = {y,z} )
assume that
A1:
y in Sphere x,r
and
A2:
z in Sphere x,r
; :: thesis: (LSeg y,z) /\ (Sphere x,r) = {y,z}
A3:
(LSeg y,z) \ {y,z} c= Ball x,r
by A1, A2, Th34;
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: {y,z} c= (LSeg y,z) /\ (Sphere x,r)
let a be
set ;
:: thesis: ( a in (LSeg y,z) /\ (Sphere x,r) implies a in {y,z} )assume A4:
a in (LSeg y,z) /\ (Sphere x,r)
;
:: thesis: a in {y,z}then A5:
a in LSeg y,
z
by XBOOLE_0:def 4;
assume
not
a in {y,z}
;
:: thesis: contradictionthen A6:
a in (LSeg y,z) \ {y,z}
by A5, XBOOLE_0:def 5;
A7:
a in Sphere x,
r
by A4, XBOOLE_0:def 4;
Ball x,
r misses Sphere x,
r
by Th19;
hence
contradiction
by A3, A6, A7, XBOOLE_0:3;
:: thesis: verum
end;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {y,z} or a in (LSeg y,z) /\ (Sphere x,r) )
assume
a in {y,z}
; :: thesis: a in (LSeg y,z) /\ (Sphere x,r)
then A8:
( a = y or a = z )
by TARSKI:def 2;
( y in LSeg y,z & z in LSeg y,z )
by RLTOPSP1:69;
hence
a in (LSeg y,z) /\ (Sphere x,r)
by A1, A2, A8, XBOOLE_0:def 4; :: thesis: verum