let SAS be AffinPlane; :: thesis: ( SAS is Pappian implies for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3 )
assume A1:
SAS is Pappian
; :: thesis: for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3
then A2:
SAS is satisfying_pap
by AFF_2:23;
let a1, a2, a3, b1, b2, b3 be Element of SAS; :: thesis: ( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 implies a3,b1 // a1,b3 )
assume that
A3:
( a1,a2 // a1,a3 & b1,b2 // b1,b3 )
and
A4:
( a1,b2 // a2,b1 & a2,b3 // a3,b2 )
; :: thesis: a3,b1 // a1,b3
A5:
( LIN a1,a2,a3 & LIN b1,b2,b3 )
by A3, AFF_1:def 1;
then consider M being Subset of SAS such that
A6:
M is being_line
and
A7:
( a1 in M & a2 in M & a3 in M )
by AFF_1:33;
consider N being Subset of SAS such that
A8:
N is being_line
and
A9:
( b1 in N & b2 in N & b3 in N )
by A5, AFF_1:33;
A10:
now assume
(
M <> N &
M // N )
;
:: thesis: a3,b1 // a1,b3then
a1,
b3 // a3,
b1
by A2, A4, A6, A7, A8, A9, AFF_2:def 13;
hence
a3,
b1 // a1,
b3
by AFF_1:13;
:: thesis: verum end;
now assume A11:
(
M <> N & not
M // N )
;
:: thesis: a3,b1 // a1,b3then consider o being
Element of the
carrier of
SAS such that A12:
(
o in M &
o in N )
by A6, A8, AFF_1:72;
A13:
now assume A14:
o = a1
;
:: thesis: a3,b1 // a1,b3then A15:
o,
b2 // b1,
a2
by A4, AFF_1:13;
A16:
now assume
b2 <> o
;
:: thesis: a3,b1 // a1,b3then
a2 in N
by A8, A9, A12, A15, AFF_1:62;
then
a2 = o
by A6, A7, A8, A11, A12, AFF_1:30;
then A17:
o,
b3 // b2,
a3
by A4, AFF_1:13;
now assume
o <> b3
;
:: thesis: a3,b1 // a1,b3then
a3 in N
by A8, A9, A12, A17, AFF_1:62;
hence
a3,
b1 // a1,
b3
by A8, A9, A12, A14, AFF_1:65;
:: thesis: verum end; hence
a3,
b1 // a1,
b3
by A14, AFF_1:12;
:: thesis: verum end; now assume A18:
b2 = o
;
:: thesis: a3,b1 // a1,b3now assume A19:
a3 <> o
;
:: thesis: a3,b1 // a1,b3
o,
a3 // a2,
b3
by A4, A18, AFF_1:13;
then
b3 in M
by A6, A7, A12, A19, AFF_1:62;
then
a1 = b3
by A6, A8, A9, A11, A12, A14, AFF_1:30;
hence
a3,
b1 // a1,
b3
by AFF_1:12;
:: thesis: verum end; hence
a3,
b1 // a1,
b3
by A8, A9, A12, A14, AFF_1:65;
:: thesis: verum end; hence
a3,
b1 // a1,
b3
by A16;
:: thesis: verum end; A20:
now assume A21:
(
o <> a1 &
b1 = o )
;
:: thesis: a3,b1 // a1,b3then A22:
o,
a2 // a1,
b2
by A4, AFF_1:13;
A23:
now assume
a2 <> o
;
:: thesis: a3,b1 // a1,b3then
b2 in M
by A6, A7, A12, A22, AFF_1:62;
then
b2 = o
by A6, A8, A9, A11, A12, AFF_1:30;
then A24:
o,
a3 // a2,
b3
by A4, AFF_1:13;
now assume
o <> a3
;
:: thesis: a3,b1 // a1,b3then
b3 in M
by A6, A7, A12, A24, AFF_1:62;
hence
a3,
b1 // a1,
b3
by A6, A7, A12, A21, AFF_1:65;
:: thesis: verum end; hence
a3,
b1 // a1,
b3
by A21, AFF_1:12;
:: thesis: verum end; now assume A25:
a2 = o
;
:: thesis: a3,b1 // a1,b3now assume A26:
b3 <> o
;
:: thesis: a3,b1 // a1,b3
o,
b3 // b2,
a3
by A4, A25, AFF_1:13;
then
a3 in N
by A8, A9, A12, A26, AFF_1:62;
then
b1 = a3
by A6, A7, A8, A11, A12, A21, AFF_1:30;
hence
a3,
b1 // a1,
b3
by AFF_1:12;
:: thesis: verum end; hence
a3,
b1 // a1,
b3
by A6, A7, A12, A21, AFF_1:65;
:: thesis: verum end; hence
a3,
b1 // a1,
b3
by A23;
:: thesis: verum end; A27:
now assume A28:
(
o <> a1 &
b1 <> o &
o = b3 )
;
:: thesis: a3,b1 // a1,b3A29:
now assume
a2 <> o
;
:: thesis: a3,b1 // a1,b3then
b2 in M
by A4, A6, A7, A12, A28, AFF_1:62;
then
b2 = o
by A6, A8, A9, A11, A12, AFF_1:30;
then
b1 in M
by A4, A6, A7, A12, A28, AFF_1:62;
hence
a3,
b1 // a1,
b3
by A6, A7, A12, A28, AFF_1:65;
:: thesis: verum end; now assume
a2 = o
;
:: thesis: a3,b1 // a1,b3then
o,
b1 // b2,
a1
by A4, AFF_1:13;
then
a1 in N
by A8, A9, A28, AFF_1:62;
hence
a3,
b1 // a1,
b3
by A6, A7, A8, A11, A12, A28, AFF_1:30;
:: thesis: verum end; hence
a3,
b1 // a1,
b3
by A29;
:: thesis: verum end; A30:
now assume A31:
(
o <> a1 &
b1 <> o &
o <> b3 &
o = a3 )
;
:: thesis: a3,b1 // a1,b3then A32:
o,
b2 // b3,
a2
by A4, AFF_1:13;
A33:
now assume
b2 <> o
;
:: thesis: a3,b1 // a1,b3then
a2 in N
by A8, A9, A12, A32, AFF_1:62;
then
a2 = o
by A6, A7, A8, A11, A12, AFF_1:30;
then
o,
b1 // b2,
a1
by A4, AFF_1:13;
then
a1 in N
by A8, A9, A12, A31, AFF_1:62;
hence
a3,
b1 // a1,
b3
by A8, A9, A12, A31, AFF_1:65;
:: thesis: verum end; now assume
b2 = o
;
:: thesis: a3,b1 // a1,b3then
b1 in M
by A4, A6, A7, A31, AFF_1:62;
hence
a3,
b1 // a1,
b3
by A6, A8, A9, A11, A12, A31, AFF_1:30;
:: thesis: verum end; hence
a3,
b1 // a1,
b3
by A33;
:: thesis: verum end; now assume A34:
(
o <> a1 &
o <> b1 &
o <> b3 &
o <> a3 )
;
:: thesis: a3,b1 // a1,b3A35:
o <> a2
proof
assume
o = a2
;
:: thesis: contradiction
then
o,
b3 // b2,
a3
by A4, AFF_1:13;
then
a3 in N
by A8, A9, A12, A34, AFF_1:62;
hence
contradiction
by A6, A7, A8, A11, A12, A34, AFF_1:30;
:: thesis: verum
end;
o <> b2
proof
assume
o = b2
;
:: thesis: contradiction
then
o,
a3 // a2,
b3
by A4, AFF_1:13;
then
b3 in M
by A6, A7, A12, A34, AFF_1:62;
hence
contradiction
by A6, A8, A9, A11, A12, A34, AFF_1:30;
:: thesis: verum
end; then
a1,
b3 // a3,
b1
by A1, A4, A6, A7, A8, A9, A11, A12, A34, A35, AFF_2:def 2;
hence
a3,
b1 // a1,
b3
by AFF_1:13;
:: thesis: verum end; hence
a3,
b1 // a1,
b3
by A13, A20, A27, A30;
:: thesis: verum end;
hence
a3,b1 // a1,b3
by A6, A7, A9, A10, AFF_1:65; :: thesis: verum