let AP be AffinPlane; :: thesis: ( AP is satisfying_pap iff AP is satisfying_pap_1 )

let M be Subset of AP; :: according to AFF_2:def 13 :: thesis: for N being Subset of AP

for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds

a,c9 // c,a9

let N be Subset of AP; :: thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds

a,c9 // c,a9

let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )

assume that

A30: M is being_line and

A31: N is being_line and

A32: a in M and

A33: b in M and

A34: c in M and

A35: ( M // N & M <> N ) and

A36: a9 in N and

A37: b9 in N and

A38: c9 in N and

A39: a,b9 // b,a9 and

A40: b,c9 // c,b9 ; :: thesis: a,c9 // c,a9

set A = Line (c,a9);

set D = Line (b,c9);

A41: b <> c9 by A33, A35, A38, AFF_1:45;

then A42: ( b in Line (b,c9) & c9 in Line (b,c9) ) by AFF_1:24;

assume A43: not a,c9 // c,a9 ; :: thesis: contradiction

then A44: c <> a9 by AFF_1:3;

then A45: c in Line (c,a9) by AFF_1:24;

A46: a9 in Line (c,a9) by A44, AFF_1:24;

A47: Line (c,a9) is being_line by A44, AFF_1:24;

then consider P being Subset of AP such that

A48: a in P and

A49: Line (c,a9) // P by AFF_1:49;

A50: a9 <> b9

P is being_line by A49, AFF_1:36;

then consider x being Element of AP such that

A54: x in Line (b,c9) and

A55: x in P by A53, A52, AFF_1:58;

LIN b,x,c9 by A53, A42, A54, AFF_1:21;

then b,x // b,c9 by AFF_1:def 1;

then A56: b,x // c,b9 by A40, A41, AFF_1:5;

a,x // c,a9 by A45, A46, A48, A49, A55, AFF_1:39;

then x in N by A29, A30, A31, A32, A33, A34, A35, A36, A37, A39, A50, A56;

then ( x = c9 or b in N ) by A31, A38, A53, A42, A54, AFF_1:18;

hence contradiction by A33, A35, A43, A45, A46, A48, A49, A55, AFF_1:39, AFF_1:45; :: thesis: verum

hereby :: thesis: ( AP is satisfying_pap_1 implies AP is satisfying_pap )

assume A29:
AP is satisfying_pap_1
; :: thesis: AP is satisfying_pap assume A1:
AP is satisfying_pap
; :: thesis: AP is satisfying_pap_1

thus AP is satisfying_pap_1 :: thesis: verum

end;thus AP is satisfying_pap_1 :: thesis: verum

proof

let M be Subset of AP; :: according to AFF_2:def 14 :: thesis: for N being Subset of AP

for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds

c9 in N

let N be Subset of AP; :: thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds

c9 in N

let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 implies c9 in N )

assume that

A2: M is being_line and

A3: N is being_line and

A4: a in M and

A5: b in M and

A6: c in M and

A7: M // N and

A8: M <> N and

A9: a9 in N and

A10: b9 in N and

A11: a,b9 // b,a9 and

A12: b,c9 // c,b9 and

A13: a,c9 // c,a9 and

A14: a9 <> b9 ; :: thesis: c9 in N

A15: c <> a9 by A6, A7, A8, A9, AFF_1:45;

set C = Line (c,b9);

A16: c <> b9 by A6, A7, A8, A10, AFF_1:45;

then Line (c,b9) is being_line by AFF_1:24;

then consider K being Subset of AP such that

A17: b in K and

A18: Line (c,b9) // K by AFF_1:49;

A19: ( c in Line (c,b9) & b9 in Line (c,b9) ) by A16, AFF_1:24;

A20: not K // N

then consider x being Element of AP such that

A21: x in K and

A22: x in N by A3, A20, AFF_1:58;

A23: b,x // c,b9 by A19, A17, A18, A21, AFF_1:39;

then a,x // c,a9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A22;

then a,x // a,c9 by A13, A15, AFF_1:5;

then LIN a,x,c9 by AFF_1:def 1;

then A24: LIN c9,x,a by AFF_1:6;

A25: a <> b

then LIN b,x,c9 by AFF_1:def 1;

then A27: LIN c9,x,b by AFF_1:6;

assume A28: not c9 in N ; :: thesis: contradiction

LIN c9,x,c9 by AFF_1:7;

then c9 in M by A2, A4, A5, A28, A25, A22, A24, A27, AFF_1:8, AFF_1:25;

then b9 in M by A2, A5, A6, A12, A26, AFF_1:48;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

end;for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds

c9 in N

let N be Subset of AP; :: thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds

c9 in N

let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 implies c9 in N )

assume that

A2: M is being_line and

A3: N is being_line and

A4: a in M and

A5: b in M and

A6: c in M and

A7: M // N and

A8: M <> N and

A9: a9 in N and

A10: b9 in N and

A11: a,b9 // b,a9 and

A12: b,c9 // c,b9 and

A13: a,c9 // c,a9 and

A14: a9 <> b9 ; :: thesis: c9 in N

A15: c <> a9 by A6, A7, A8, A9, AFF_1:45;

set C = Line (c,b9);

A16: c <> b9 by A6, A7, A8, A10, AFF_1:45;

then Line (c,b9) is being_line by AFF_1:24;

then consider K being Subset of AP such that

A17: b in K and

A18: Line (c,b9) // K by AFF_1:49;

A19: ( c in Line (c,b9) & b9 in Line (c,b9) ) by A16, AFF_1:24;

A20: not K // N

proof

K is being_line
by A18, AFF_1:36;
assume
K // N
; :: thesis: contradiction

then Line (c,b9) // N by A18, AFF_1:44;

then Line (c,b9) // M by A7, AFF_1:44;

then b9 in M by A6, A19, AFF_1:45;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

end;then Line (c,b9) // N by A18, AFF_1:44;

then Line (c,b9) // M by A7, AFF_1:44;

then b9 in M by A6, A19, AFF_1:45;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

then consider x being Element of AP such that

A21: x in K and

A22: x in N by A3, A20, AFF_1:58;

A23: b,x // c,b9 by A19, A17, A18, A21, AFF_1:39;

then a,x // c,a9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A22;

then a,x // a,c9 by A13, A15, AFF_1:5;

then LIN a,x,c9 by AFF_1:def 1;

then A24: LIN c9,x,a by AFF_1:6;

A25: a <> b

proof

A26:
c9 <> b
assume
a = b
; :: thesis: contradiction

then LIN a,b9,a9 by A11, AFF_1:def 1;

then LIN a9,b9,a by AFF_1:6;

then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:25;

hence contradiction by A4, A7, A8, A14, AFF_1:45; :: thesis: verum

end;then LIN a,b9,a9 by A11, AFF_1:def 1;

then LIN a9,b9,a by AFF_1:6;

then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:25;

hence contradiction by A4, A7, A8, A14, AFF_1:45; :: thesis: verum

proof

b,x // b,c9
by A12, A16, A23, AFF_1:5;
assume
c9 = b
; :: thesis: contradiction

then a9 in M by A2, A4, A5, A6, A13, A25, AFF_1:48;

hence contradiction by A7, A8, A9, AFF_1:45; :: thesis: verum

end;then a9 in M by A2, A4, A5, A6, A13, A25, AFF_1:48;

hence contradiction by A7, A8, A9, AFF_1:45; :: thesis: verum

then LIN b,x,c9 by AFF_1:def 1;

then A27: LIN c9,x,b by AFF_1:6;

assume A28: not c9 in N ; :: thesis: contradiction

LIN c9,x,c9 by AFF_1:7;

then c9 in M by A2, A4, A5, A28, A25, A22, A24, A27, AFF_1:8, AFF_1:25;

then b9 in M by A2, A5, A6, A12, A26, AFF_1:48;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

let M be Subset of AP; :: according to AFF_2:def 13 :: thesis: for N being Subset of AP

for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds

a,c9 // c,a9

let N be Subset of AP; :: thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds

a,c9 // c,a9

let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )

assume that

A30: M is being_line and

A31: N is being_line and

A32: a in M and

A33: b in M and

A34: c in M and

A35: ( M // N & M <> N ) and

A36: a9 in N and

A37: b9 in N and

A38: c9 in N and

A39: a,b9 // b,a9 and

A40: b,c9 // c,b9 ; :: thesis: a,c9 // c,a9

set A = Line (c,a9);

set D = Line (b,c9);

A41: b <> c9 by A33, A35, A38, AFF_1:45;

then A42: ( b in Line (b,c9) & c9 in Line (b,c9) ) by AFF_1:24;

assume A43: not a,c9 // c,a9 ; :: thesis: contradiction

then A44: c <> a9 by AFF_1:3;

then A45: c in Line (c,a9) by AFF_1:24;

A46: a9 in Line (c,a9) by A44, AFF_1:24;

A47: Line (c,a9) is being_line by A44, AFF_1:24;

then consider P being Subset of AP such that

A48: a in P and

A49: Line (c,a9) // P by AFF_1:49;

A50: a9 <> b9

proof

A52:
not Line (b,c9) // P
assume A51:
a9 = b9
; :: thesis: contradiction

then a9,a // a9,b by A39, AFF_1:4;

then LIN a9,a,b by AFF_1:def 1;

then LIN a,b,a9 by AFF_1:6;

then ( a = b or a9 in M ) by A30, A32, A33, AFF_1:25;

hence contradiction by A35, A36, A40, A43, A51, AFF_1:45; :: thesis: verum

end;then a9,a // a9,b by A39, AFF_1:4;

then LIN a9,a,b by AFF_1:def 1;

then LIN a,b,a9 by AFF_1:6;

then ( a = b or a9 in M ) by A30, A32, A33, AFF_1:25;

hence contradiction by A35, A36, A40, A43, A51, AFF_1:45; :: thesis: verum

proof

A53:
Line (b,c9) is being_line
by A41, AFF_1:24;
assume
Line (b,c9) // P
; :: thesis: contradiction

then c,b9 // P by A40, A41, A42, AFF_1:32, AFF_1:40;

then c,b9 // Line (c,a9) by A49, AFF_1:43;

then b9 in Line (c,a9) by A47, A45, AFF_1:23;

then c in N by A31, A36, A37, A50, A47, A45, A46, AFF_1:18;

hence contradiction by A34, A35, AFF_1:45; :: thesis: verum

end;then c,b9 // P by A40, A41, A42, AFF_1:32, AFF_1:40;

then c,b9 // Line (c,a9) by A49, AFF_1:43;

then b9 in Line (c,a9) by A47, A45, AFF_1:23;

then c in N by A31, A36, A37, A50, A47, A45, A46, AFF_1:18;

hence contradiction by A34, A35, AFF_1:45; :: thesis: verum

P is being_line by A49, AFF_1:36;

then consider x being Element of AP such that

A54: x in Line (b,c9) and

A55: x in P by A53, A52, AFF_1:58;

LIN b,x,c9 by A53, A42, A54, AFF_1:21;

then b,x // b,c9 by AFF_1:def 1;

then A56: b,x // c,b9 by A40, A41, AFF_1:5;

a,x // c,a9 by A45, A46, A48, A49, A55, AFF_1:39;

then x in N by A29, A30, A31, A32, A33, A34, A35, A36, A37, A39, A50, A56;

then ( x = c9 or b in N ) by A31, A38, A53, A42, A54, AFF_1:18;

hence contradiction by A33, A35, A43, A45, A46, A48, A49, A55, AFF_1:39, AFF_1:45; :: thesis: verum