let n be Nat; for r being Real
for y, z, x 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; for y, z, x 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, z, x 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:68;
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 Th32;
hereby TARSKI:def 3,
XBOOLE_0:def 10 {y,z} c= (LSeg (y,z)) /\ (Sphere (x,r))
let a be
object ;
( 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 Th17;
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 object ; 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