let AS be AffinSpace; for a, b being Element of AS
for K, P, Q being Subset of AS st K is being_line & P is being_line & Q is being_line & a in Plane (K,P) & b in Plane (K,P) & a <> b & a in Q & b in Q holds
Q c= Plane (K,P)
let a, b be Element of AS; for K, P, Q being Subset of AS st K is being_line & P is being_line & Q is being_line & a in Plane (K,P) & b in Plane (K,P) & a <> b & a in Q & b in Q holds
Q c= Plane (K,P)
let K, P, Q be Subset of AS; ( K is being_line & P is being_line & Q is being_line & a in Plane (K,P) & b in Plane (K,P) & a <> b & a in Q & b in Q implies Q c= Plane (K,P) )
assume that
A1:
K is being_line
and
A2:
P is being_line
and
A3:
Q is being_line
and
A4:
a in Plane (K,P)
and
A5:
b in Plane (K,P)
and
A6:
a <> b
and
A7:
a in Q
and
A8:
b in Q
; Q c= Plane (K,P)
let x be object ; TARSKI:def 3 ( not x in Q or x in Plane (K,P) )
assume A9:
x in Q
; x in Plane (K,P)
then reconsider c = x as Element of AS ;
consider a9 being Element of AS such that
A10:
a,a9 // K
and
A11:
a9 in P
by A4, Lm3;
consider Y being Subset of AS such that
A12:
b in Y
and
A13:
K // Y
by A1, AFF_1:49;
consider X being Subset of AS such that
A14:
a in X
and
A15:
K // X
by A1, AFF_1:49;
consider b9 being Element of AS such that
A16:
b,b9 // K
and
A17:
b9 in P
by A5, Lm3;
b,b9 // Y
by A16, A13, AFF_1:43;
then A18:
b9 in Y
by A12, Th2;
a,a9 // X
by A10, A15, AFF_1:43;
then A19:
a9 in X
by A14, Th2;
A20:
X // Y
by A15, A13, AFF_1:44;
A21:
now ( X <> Y implies x in Plane (K,P) )A22:
now ( ex q being Element of AS st
( q in P & q in Q & not P // Q ) implies x in Plane (K,P) )given q being
Element of
AS such that A23:
q in P
and A24:
q in Q
and A25:
not
P // Q
;
x in Plane (K,P)A26:
P <> Q
by A2, A25, AFF_1:41;
A27:
now ( q <> b implies x in Plane (K,P) )assume A28:
q <> b
;
x in Plane (K,P)then A29:
b <> b9
by A2, A3, A8, A17, A23, A24, A26, AFF_1:18;
A30:
now ( q <> b9 implies x in Plane (K,P) )A31:
q,
b9 // P
by A2, A17, A23, AFF_1:23;
LIN q,
b,
c
by A3, A8, A9, A24, AFF_1:21;
then consider c9 being
Element of
AS such that A32:
LIN q,
b9,
c9
and A33:
b,
b9 // c,
c9
by A28, Th1;
assume A34:
q <> b9
;
x in Plane (K,P)
q,
b9 // q,
c9
by A32, AFF_1:def 1;
then
q,
c9 // P
by A34, A31, AFF_1:32;
then A35:
c9 in P
by A23, Th2;
c,
c9 // K
by A16, A29, A33, AFF_1:32;
hence
x in Plane (
K,
P)
by A35;
verum end; now ( q = b9 implies x in Plane (K,P) )assume A36:
q = b9
;
x in Plane (K,P)
b,
q // Q
by A3, A8, A24, AFF_1:23;
then
Q c= Plane (
K,
P)
by A4, A7, A16, A28, A36, Lm4, AFF_1:53;
hence
x in Plane (
K,
P)
by A9;
verum end; hence
x in Plane (
K,
P)
by A30;
verum end; now ( q <> a implies x in Plane (K,P) )assume A37:
q <> a
;
x in Plane (K,P)then A38:
a <> a9
by A2, A3, A7, A11, A23, A24, A26, AFF_1:18;
A39:
now ( q <> a9 implies x in Plane (K,P) )A40:
q,
a9 // P
by A2, A11, A23, AFF_1:23;
LIN q,
a,
c
by A3, A7, A9, A24, AFF_1:21;
then consider c9 being
Element of
AS such that A41:
LIN q,
a9,
c9
and A42:
a,
a9 // c,
c9
by A37, Th1;
assume A43:
q <> a9
;
x in Plane (K,P)
q,
a9 // q,
c9
by A41, AFF_1:def 1;
then
q,
c9 // P
by A43, A40, AFF_1:32;
then A44:
c9 in P
by A23, Th2;
c,
c9 // K
by A10, A38, A42, AFF_1:32;
hence
x in Plane (
K,
P)
by A44;
verum end; now ( q = a9 implies x in Plane (K,P) )assume A45:
q = a9
;
x in Plane (K,P)
a,
q // Q
by A3, A7, A24, AFF_1:23;
then
Q c= Plane (
K,
P)
by A4, A7, A10, A37, A45, Lm4, AFF_1:53;
hence
x in Plane (
K,
P)
by A9;
verum end; hence
x in Plane (
K,
P)
by A39;
verum end; hence
x in Plane (
K,
P)
by A6, A27;
verum end; A46:
now ( P // Q implies x in Plane (K,P) )assume A47:
P // Q
;
x in Plane (K,P)A48:
now ( P <> Q implies x in Plane (K,P) )assume
P <> Q
;
x in Plane (K,P)then A49:
b <> b9
by A8, A17, A47, AFF_1:45;
now ( c <> b implies x in Plane (K,P) )assume A50:
c <> b
;
x in Plane (K,P)consider c9 being
Element of
AS such that A51:
b,
c // b9,
c9
and A52:
b,
b9 // c,
c9
by DIRAF:40;
b,
c // Q
by A3, A8, A9, AFF_1:23;
then
b9,
c9 // Q
by A50, A51, AFF_1:32;
then
b9,
c9 // P
by A47, AFF_1:43;
then A53:
c9 in P
by A17, Th2;
c,
c9 // K
by A16, A49, A52, AFF_1:32;
hence
x in Plane (
K,
P)
by A53;
verum end; hence
x in Plane (
K,
P)
by A5;
verum end; hence
x in Plane (
K,
P)
by A48;
verum end; assume
X <> Y
;
x in Plane (K,P)then
(
P // Q or ex
q being
Element of
AS st
(
q in P &
q in Q ) )
by A2, A3, A7, A8, A11, A17, A14, A12, A20, A19, A18, Th18;
hence
x in Plane (
K,
P)
by A46, A22;
verum end;
A55:
X is being_line
by A10, A15, AFF_1:26, AFF_1:43;
now ( X = Y implies x in Plane (K,P) )assume
X = Y
;
x in Plane (K,P)then
Q = X
by A3, A6, A7, A8, A14, A12, A55, AFF_1:18;
then
Q c= Plane (
K,
P)
by A4, A7, A15, Lm4;
hence
x in Plane (
K,
P)
by A9;
verum end;
hence
x in Plane (K,P)
by A21; verum