let AS be AffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: Q c= Plane (K,P)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in Plane (K,P) )

assume A9: x in Q ; :: thesis: 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;

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: Q c= Plane (K,P)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in Plane (K,P) )

assume A9: x in Q ; :: thesis: 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 :: thesis: ( X <> Y implies 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; :: thesis: verum

end;

A55:
X is being_line
by A10, A15, AFF_1:26, AFF_1:43;A22: now :: thesis: ( ex q being Element of AS st

( q in P & q in Q & not P // Q ) implies x in Plane (K,P) )

( 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 ; :: thesis: x in Plane (K,P)

A26: P <> Q by A2, A25, AFF_1:41;

end;A24: q in Q and

A25: not P // Q ; :: thesis: x in Plane (K,P)

A26: P <> Q by A2, A25, AFF_1:41;

A27: now :: thesis: ( q <> b implies x in Plane (K,P) )

assume A28:
q <> b
; :: thesis: x in Plane (K,P)

then A29: b <> b9 by A2, A3, A8, A17, A23, A24, A26, AFF_1:18;

end;then A29: b <> b9 by A2, A3, A8, A17, A23, A24, A26, AFF_1:18;

A30: now :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;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 ; :: thesis: 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; :: thesis: verum

now :: thesis: ( q = b9 implies x in Plane (K,P) )

hence
x in Plane (K,P)
by A30; :: thesis: verumassume A36:
q = b9
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

now :: thesis: ( q <> a implies x in Plane (K,P) )

hence
x in Plane (K,P)
by A6, A27; :: thesis: verumassume A37:
q <> a
; :: thesis: x in Plane (K,P)

then A38: a <> a9 by A2, A3, A7, A11, A23, A24, A26, AFF_1:18;

end;then A38: a <> a9 by A2, A3, A7, A11, A23, A24, A26, AFF_1:18;

A39: now :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;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 ; :: thesis: 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; :: thesis: verum

now :: thesis: ( q = a9 implies x in Plane (K,P) )

hence
x in Plane (K,P)
by A39; :: thesis: verumassume A45:
q = a9
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A46: now :: thesis: ( P // Q implies x in Plane (K,P) )

assume
X <> Y
; :: thesis: x in Plane (K,P)assume A47:
P // Q
; :: thesis: x in Plane (K,P)

end;A48: now :: thesis: ( P <> Q implies x in Plane (K,P) )

assume
P <> Q
; :: thesis: x in Plane (K,P)

then A49: b <> b9 by A8, A17, A47, AFF_1:45;

end;then A49: b <> b9 by A8, A17, A47, AFF_1:45;

now :: thesis: ( c <> b implies x in Plane (K,P) )

hence
x in Plane (K,P)
by A5; :: thesis: verumassume A50:
c <> b
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

now :: thesis: ( P = Q implies x in Plane (K,P) )

hence
x in Plane (K,P)
by A48; :: thesis: verumassume A54:
P = Q
; :: thesis: x in Plane (K,P)

c,c // K by A1, AFF_1:33;

hence x in Plane (K,P) by A9, A54; :: thesis: verum

end;c,c // K by A1, AFF_1:33;

hence x in Plane (K,P) by A9, A54; :: thesis: verum

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; :: thesis: verum

now :: thesis: ( X = Y implies x in Plane (K,P) )

hence
x in Plane (K,P)
by A21; :: thesis: verumassume
X = Y
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum