let X, Y be Subset of TarskiEuclid2Space; :: thesis: for a being Element of TarskiEuclid2Space st ( for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y ) & not X is empty & not Y is empty & ( X is trivial implies X <> {a} ) holds
ex b being Element of TarskiEuclid2Space st
( X c= Line ((Tn2TR a),(Tn2TR b)) & Y c= Line ((Tn2TR a),(Tn2TR b)) )
let a be Element of TarskiEuclid2Space; :: thesis: ( ( for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y ) & not X is empty & not Y is empty & ( X is trivial implies X <> {a} ) implies ex b being Element of TarskiEuclid2Space st
( X c= Line ((Tn2TR a),(Tn2TR b)) & Y c= Line ((Tn2TR a),(Tn2TR b)) ) )
assume that
A1: for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y and
A1A: not X is empty and
A1B: not Y is empty and
A3: ( X is trivial implies X <> {a} ) ; :: thesis: ex b being Element of TarskiEuclid2Space st
( X c= Line ((Tn2TR a),(Tn2TR b)) & Y c= Line ((Tn2TR a),(Tn2TR b)) )
consider x0 being object such that
K1: x0 in X by A1A;
reconsider x0 = x0 as Element of TarskiEuclid2Space by K1;
consider c being object such that
MM: c in Y by A1B;
reconsider c = c as Element of TarskiEuclid2Space by MM;
V1: X c= LSeg ((Tn2TR a),(Tn2TR c))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in LSeg ((Tn2TR a),(Tn2TR c)) )
assume DA: x in X ; :: thesis: x in LSeg ((Tn2TR a),(Tn2TR c))
then reconsider x1 = x as Element of TarskiEuclid2Space ;
Tn2TR x1 in LSeg ((Tn2TR a),(Tn2TR c)) by ThConv6, A1, DA, MM;
hence x in LSeg ((Tn2TR a),(Tn2TR c)) ; :: thesis: verum
end;
t2: LSeg ((Tn2TR a),(Tn2TR c)) c= Line ((Tn2TR a),(Tn2TR c)) by RLTOPSP1:73;
then T1: X c= Line ((Tn2TR a),(Tn2TR c)) by V1;
T2: x0 in Line ((Tn2TR a),(Tn2TR c)) by t2, V1, K1;
Y c= Line ((Tn2TR a),(Tn2TR c))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in Line ((Tn2TR a),(Tn2TR c)) )
assume V2: y in Y ; :: thesis: y in Line ((Tn2TR a),(Tn2TR c))
then reconsider y0 = y as Element of TarskiEuclid2Space ;
per cases ( x0 = a or x0 <> a ) ;
suppose MU: x0 = a ; :: thesis: y in Line ((Tn2TR a),(Tn2TR c))
per cases ( X is trivial or not X is trivial ) ;
suppose X is trivial ; :: thesis: y in Line ((Tn2TR a),(Tn2TR c))
then consider xx being object such that
KL: X = {xx} by A1A, ZFMISC_1:131;
thus y in Line ((Tn2TR a),(Tn2TR c)) by MU, K1, KL, TARSKI:def 1, A3; :: thesis: verum
end;
suppose not X is trivial ; :: thesis: y in Line ((Tn2TR a),(Tn2TR c))
then consider a0, b0 being object such that
LO1: a0 in X and
LO2: b0 in X and
LO3: a0 <> b0 ;
ex x1 being object st
( x1 in X & x1 <> a )
proof
assume AA: for x1 being object holds
( not x1 in X or x1 = a ) ; :: thesis: contradiction
( a0 <> a or b0 <> a ) by LO3;
hence contradiction by LO1, LO2, AA; :: thesis: verum
end;
then consider x1 being object such that
K1: x1 in X and
VAL: x1 <> a ;
reconsider x1 = x1 as Element of TarskiEuclid2Space by K1;
N1: Tn2TR x1 in LSeg ((Tn2TR a),(Tn2TR y0)) by ThConv6, V2, K1, A1;
n2: LSeg ((Tn2TR a),(Tn2TR y0)) c= Line ((Tn2TR a),(Tn2TR y0)) by RLTOPSP1:73;
Tn2TR a in Line ((Tn2TR a),(Tn2TR y0)) by RLTOPSP1:72;
then ff: Line ((Tn2TR x1),(Tn2TR a)) = Line ((Tn2TR a),(Tn2TR y0)) by N1, n2, VAL, RLTOPSP1:75;
Tn2TR a in Line ((Tn2TR a),(Tn2TR c)) by RLTOPSP1:72;
then Line ((Tn2TR a),(Tn2TR x1)) c= Line ((Tn2TR a),(Tn2TR c)) by K1, T1, RLTOPSP1:74;
hence y in Line ((Tn2TR a),(Tn2TR c)) by ff, RLTOPSP1:72; :: thesis: verum
end;
end;
end;
suppose VAL: x0 <> a ; :: thesis: y in Line ((Tn2TR a),(Tn2TR c))
N1: Tn2TR x0 in LSeg ((Tn2TR a),(Tn2TR y0)) by ThConv6, V2, K1, A1;
n2: LSeg ((Tn2TR a),(Tn2TR y0)) c= Line ((Tn2TR a),(Tn2TR y0)) by RLTOPSP1:73;
Tn2TR a in Line ((Tn2TR a),(Tn2TR y0)) by RLTOPSP1:72;
then ff: Line ((Tn2TR x0),(Tn2TR a)) = Line ((Tn2TR a),(Tn2TR y0)) by N1, n2, VAL, RLTOPSP1:75;
Tn2TR a in Line ((Tn2TR a),(Tn2TR c)) by RLTOPSP1:72;
then Line ((Tn2TR a),(Tn2TR x0)) c= Line ((Tn2TR a),(Tn2TR c)) by T2, RLTOPSP1:74;
hence y in Line ((Tn2TR a),(Tn2TR c)) by ff, RLTOPSP1:72; :: thesis: verum
end;
end;
end;
hence ex b being Element of TarskiEuclid2Space st
( X c= Line ((Tn2TR a),(Tn2TR b)) & Y c= Line ((Tn2TR a),(Tn2TR b)) ) by T1; :: thesis: verum