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;
A21: now :: thesis: ( X <> Y implies x in Plane (K,P) )
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) )
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;
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;
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;
now :: thesis: ( q = b9 implies x in Plane (K,P) )
assume 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;
hence x in Plane (K,P) by A30; :: thesis: verum
end;
now :: thesis: ( q <> a implies x in Plane (K,P) )
assume A37: q <> a ; :: thesis: x in Plane (K,P)
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;
now :: thesis: ( q = a9 implies x in Plane (K,P) )
assume 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;
hence x in Plane (K,P) by A39; :: thesis: verum
end;
hence x in Plane (K,P) by A6, A27; :: thesis: verum
end;
A46: now :: thesis: ( P // Q implies x in Plane (K,P) )
assume A47: P // Q ; :: thesis: x in Plane (K,P)
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;
now :: thesis: ( c <> b implies x in Plane (K,P) )
assume 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;
hence x in Plane (K,P) by A5; :: thesis: verum
end;
now :: thesis: ( P = Q implies x in Plane (K,P) )
assume 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;
hence x in Plane (K,P) by A48; :: thesis: verum
end;
assume X <> Y ; :: thesis: 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;
now :: thesis: ( X = Y implies x in Plane (K,P) )
assume 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;
hence x in Plane (K,P) by A21; :: thesis: verum