let X be AffinPlane; :: thesis: ( X is Pappian iff X is satisfying_major_indirect_Scherungssatz )
A1: ( X is Pappian implies X is satisfying_major_indirect_Scherungssatz )

proof

assume A2: X is Pappian ; :: thesis: X is satisfying_major_indirect_Scherungssatz
then A3: X is Desarguesian by AFF_2:11;

now :: thesis: for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4

let o, a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; :: thesis: for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4
let M, N be Subset of X; :: thesis: ( M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 )
assume that
A4: M is being_line and
A5: N is being_line and
A6: o in M and
A7: o in N and
A8: a1 in M and
A9: a3 in M and
A10: b2 in M and
A11: b4 in M and
A12: a2 in N and
A13: a4 in N and
A14: b1 in N and
A15: b3 in N and
A16: not a4 in M and
A17: not a2 in M and
A18: not b1 in M and
A19: not b3 in M and
A20: not a1 in N and
A21: not a3 in N and
A22: not b2 in N and
A23: not b4 in N and
A24: a3,a2 // b3,b2 and
A25: a2,a1 // b2,b1 and
A26: a1,a4 // b1,b4 ; :: thesis: a3,a4 // b3,b4

A27: now :: thesis: ( a1 <> a3 & a2 <> a4 implies a3,a4 // b3,b4 )

assume that
A28: a1 <> a3 and
A29: a2 <> a4 ; :: thesis: a3,a4 // b3,b4
ex x, y, z being Element of X st
( LIN x,y,z & x <> y & x <> z & y <> z )

proof

o,a1 // o,a3 by A4, A6, A8, A9, AFF_1:39, AFF_1:41;
then A30: LIN o,a1,a3 by AFF_1:def 1;
assume for x, y, z being Element of X holds
( not LIN x,y,z or not x <> y or not x <> z or not y <> z ) ; :: thesis: contradiction
hence contradiction by A7, A20, A21, A28, A30; :: thesis: verum

end;

then consider d being Element of X such that
A31: LIN a2,a1,d and
A32: a2 <> d and
A33: a1 <> d by TRANSLAC:1;
A34: a2,a1 // a2,d by A31, AFF_1:def 1;
A35: ex c2 being Element of X st
( c2 in M & a2,a3 // b1,c2 )

proof

consider e2 being Element of X such that
A36: a1,a3 // a1,e2 and
A37: a1 <> e2 by DIRAF:40;
consider e1 being Element of X such that
A38: a2,a3 // b1,e1 and
A39: b1 <> e1 by DIRAF:40;
not b1,e1 // a1,e2

proof

assume b1,e1 // a1,e2 ; :: thesis: contradiction
then a2,a3 // a1,e2 by A38, A39, AFF_1:5;
then a2,a3 // a1,a3 by A36, A37, AFF_1:5;
then a3,a1 // a3,a2 by AFF_1:4;
then LIN a3,a1,a2 by AFF_1:def 1;
hence contradiction by A4, A8, A9, A17, A28, AFF_1:25; :: thesis: verum

end;

then consider c2 being Element of X such that
A40: LIN b1,e1,c2 and
A41: LIN a1,e2,c2 by AFF_1:60;
a1,e2 // a1,c2 by A41, AFF_1:def 1;
then a1,a3 // a1,c2 by A36, A37, AFF_1:5;
then A42: LIN a1,a3,c2 by AFF_1:def 1;
take c2 ; :: thesis: ( c2 in M & a2,a3 // b1,c2 )
b1,e1 // b1,c2 by A40, AFF_1:def 1;
hence ( c2 in M & a2,a3 // b1,c2 ) by A4, A8, A9, A28, A38, A39, A42, AFF_1:5, AFF_1:25; :: thesis: verum

end;

A43: ex c1 being Element of X st
( c1 in N & a1,a4 // b2,c1 )

proof

consider e2 being Element of X such that
A44: a2,a4 // a2,e2 and
A45: a2 <> e2 by DIRAF:40;
consider e1 being Element of X such that
A46: a1,a4 // b2,e1 and
A47: b2 <> e1 by DIRAF:40;
not b2,e1 // a2,e2

proof

assume b2,e1 // a2,e2 ; :: thesis: contradiction
then a1,a4 // a2,e2 by A46, A47, AFF_1:5;
then a1,a4 // a2,a4 by A44, A45, AFF_1:5;
then a4,a2 // a4,a1 by AFF_1:4;
then LIN a4,a2,a1 by AFF_1:def 1;
hence contradiction by A5, A12, A13, A20, A29, AFF_1:25; :: thesis: verum

end;

then consider c1 being Element of X such that
A48: LIN b2,e1,c1 and
A49: LIN a2,e2,c1 by AFF_1:60;
a2,e2 // a2,c1 by A49, AFF_1:def 1;
then a2,a4 // a2,c1 by A44, A45, AFF_1:5;
then A50: LIN a2,a4,c1 by AFF_1:def 1;
take c1 ; :: thesis: ( c1 in N & a1,a4 // b2,c1 )
b2,e1 // b2,c1 by A48, AFF_1:def 1;
hence ( c1 in N & a1,a4 // b2,c1 ) by A5, A12, A13, A29, A46, A47, A50, AFF_1:5, AFF_1:25; :: thesis: verum

end;

consider c2 being Element of X such that
A51: c2 in M and
A52: a2,a3 // b1,c2 by A35;
consider c1 being Element of X such that
A53: c1 in N and
A54: a1,a4 // b2,c1 by A43;
b1,b4 // b2,c1 by A8, A16, A26, A54, AFF_1:5;
then A55: b4,b1 // b2,c1 by AFF_1:4;
A56: ( o <> c1 & o <> c2 )

proof

A57: now :: thesis: not o = c2

assume o = c2 ; :: thesis: contradiction
then A58: o,b1 // a2,a3 by A52, AFF_1:4;
o,b1 // a2,a4 by A5, A7, A12, A13, A14, AFF_1:39, AFF_1:41;
then a2,a4 // a2,a3 by A6, A18, A58, AFF_1:5;
then LIN a2,a4,a3 by AFF_1:def 1;
hence contradiction by A5, A12, A13, A21, A29, AFF_1:25; :: thesis: verum

end;

A59: now :: thesis: not o = c1

assume o = c1 ; :: thesis: contradiction
then A60: o,b2 // a1,a4 by A54, AFF_1:4;
o,b2 // a1,a3 by A4, A6, A8, A9, A10, AFF_1:39, AFF_1:41;
then a1,a3 // a1,a4 by A7, A22, A60, AFF_1:5;
then LIN a1,a3,a4 by AFF_1:def 1;
hence contradiction by A4, A8, A9, A16, A28, AFF_1:25; :: thesis: verum

end;

assume ( not o <> c1 or not o <> c2 ) ; :: thesis: contradiction
hence contradiction by A59, A57; :: thesis: verum

end;

a3,a2 // c2,b1 by A52, AFF_1:4;
then b3,b2 // c2,b1 by A9, A17, A24, AFF_1:5;
then b2,b3 // c2,b1 by AFF_1:4;
then A61: b4,b3 // c2,c1 by A2, A4, A5, A6, A7, A10, A11, A14, A15, A18, A19, A22, A23, A53, A51, A56, A55, AFF_2:def 2;
LIN a1,a2,d by A31, AFF_1:6;
then a1,a2 // a1,d by AFF_1:def 1;
then a2,a1 // a1,d by AFF_1:4;
then A62: b2,b1 // a1,d by A8, A17, A25, AFF_1:5;
A63: b1 <> b3

proof

assume b1 = b3 ; :: thesis: contradiction
then b2,b1 // a2,a3 by A24, AFF_1:4;
then A64: a2,a1 // a2,a3 by A10, A18, A25, AFF_1:5;
o,a1 // o,a3 by A4, A6, A8, A9, AFF_1:39, AFF_1:41;
then LIN o,a1,a3 by AFF_1:def 1;
hence contradiction by A5, A6, A7, A12, A17, A20, A28, A64, AFF_1:14, AFF_1:25; :: thesis: verum

end;

A65: c1 <> c2

proof

A66: b1 <> c1

proof

assume b1 = c1 ; :: thesis: contradiction
then a1,a4 // a2,a1 by A10, A18, A25, A54, AFF_1:5;
then a1,a4 // a1,a2 by AFF_1:4;
then LIN a1,a4,a2 by AFF_1:def 1;
then LIN a2,a4,a1 by AFF_1:6;
hence contradiction by A5, A12, A13, A20, A29, AFF_1:25; :: thesis: verum

end;

assume c1 = c2 ; :: thesis: contradiction
then a3,a2 // b1,c1 by A52, AFF_1:4;
then A67: b3,b2 // b1,c1 by A9, A17, A24, AFF_1:5;
b1,c1 // b3,b1 by A5, A14, A15, A53, AFF_1:39, AFF_1:41;
then b3,b1 // b3,b2 by A67, A66, AFF_1:5;
then LIN b3,b1,b2 by AFF_1:def 1;
hence contradiction by A5, A14, A15, A22, A63, AFF_1:25; :: thesis: verum

end;

LIN o,d,d by AFF_1:7;
then consider Y being Subset of X such that
A68: Y is being_line and
A69: o in Y and
A70: d in Y and
d in Y by AFF_1:21;
A71: ( M <> N & M <> Y & N <> Y )

proof

A72: now :: thesis: not N = Y

assume A73: N = Y ; :: thesis: contradiction
LIN a2,d,a1 by A31, AFF_1:6;
hence contradiction by A5, A12, A20, A32, A70, A73, AFF_1:25; :: thesis: verum

end;

A74: now :: thesis: not M = Y

assume A75: M = Y ; :: thesis: contradiction
LIN a1,d,a2 by A31, AFF_1:6;
hence contradiction by A4, A8, A17, A33, A70, A75, AFF_1:25; :: thesis: verum

end;

assume ( not M <> N or not M <> Y or not N <> Y ) ; :: thesis: contradiction
hence contradiction by A13, A16, A74, A72; :: thesis: verum

end;

A76: o <> d

proof

assume o = d ; :: thesis: contradiction
then LIN o,a1,a2 by A31, AFF_1:6;
hence contradiction by A4, A6, A7, A8, A17, A20, AFF_1:25; :: thesis: verum

end;

ex d1 being Element of X st
( LIN b1,b2,d1 & d1 in Y )

proof

consider e2 being Element of X such that
A77: o,d // o,e2 and
A78: o <> e2 by DIRAF:40;
consider e1 being Element of X such that
A79: b1,b2 // b1,e1 and
A80: b1 <> e1 by DIRAF:40;
not b1,e1 // o,e2

proof

assume b1,e1 // o,e2 ; :: thesis: contradiction
then b1,b2 // o,e2 by A79, A80, AFF_1:5;
then b1,b2 // o,d by A77, A78, AFF_1:5;
then b2,b1 // o,d by AFF_1:4;
then A81: a2,a1 // o,d by A10, A18, A25, AFF_1:5;
a2,a1 // a2,d by A31, AFF_1:def 1;
then a2,d // o,d by A8, A17, A81, AFF_1:5;
then d,o // d,a2 by AFF_1:4;
then LIN d,o,a2 by AFF_1:def 1;
then A82: LIN o,a2,d by AFF_1:6;
LIN a1,a2,d by A31, AFF_1:6;
then a1,a2 // a1,d by AFF_1:def 1;
hence contradiction by A4, A6, A7, A8, A17, A20, A32, A82, AFF_1:14, AFF_1:25; :: thesis: verum

end;

then consider d1 being Element of X such that
A83: LIN b1,e1,d1 and
A84: LIN o,e2,d1 by AFF_1:60;
o,e2 // o,d1 by A84, AFF_1:def 1;
then o,d // o,d1 by A77, A78, AFF_1:5;
then A85: LIN o,d,d1 by AFF_1:def 1;
take d1 ; :: thesis: ( LIN b1,b2,d1 & d1 in Y )
b1,e1 // b1,d1 by A83, AFF_1:def 1;
then b1,b2 // b1,d1 by A79, A80, AFF_1:5;
hence ( LIN b1,b2,d1 & d1 in Y ) by A76, A68, A69, A70, A85, AFF_1:25, AFF_1:def 1; :: thesis: verum

end;

then consider d1 being Element of X such that
A86: LIN b1,b2,d1 and
A87: d1 in Y ;
LIN b2,b1,d1 by A86, AFF_1:6;
then b2,b1 // b2,d1 by AFF_1:def 1;
then a1,d // b2,d1 by A10, A18, A62, AFF_1:5;
then A88: d,a4 // d1,c1 by A3, A4, A5, A6, A7, A8, A10, A13, A16, A20, A76, A68, A69, A70, A87, A53, A54, A71, AFF_2:def 4;
b1,b2 // b1,d1 by A86, AFF_1:def 1;
then b2,b1 // b1,d1 by AFF_1:4;
then a2,a1 // b1,d1 by A10, A18, A25, AFF_1:5;
then a2,d // b1,d1 by A8, A17, A34, AFF_1:5;
then d,a3 // d1,c2 by A3, A4, A5, A6, A7, A9, A12, A14, A17, A21, A76, A68, A69, A70, A87, A51, A52, A71, AFF_2:def 4;
then a3,a4 // c2,c1 by A3, A4, A5, A6, A7, A9, A13, A16, A21, A76, A68, A69, A70, A87, A53, A51, A71, A88, AFF_2:def 4;
then b4,b3 // a3,a4 by A65, A61, AFF_1:5;
hence a3,a4 // b3,b4 by AFF_1:4; :: thesis: verum

end;

now :: thesis: ( ( a1 = a3 or a2 = a4 ) implies a3,a4 // b3,b4 )

A89: now :: thesis: ( a2 = a4 implies a3,a4 // b3,b4 )

o,b2 // o,b4 by A4, A6, A10, A11, AFF_1:39, AFF_1:41;
then A90: LIN o,b2,b4 by AFF_1:def 1;
assume A91: a2 = a4 ; :: thesis: a3,a4 // b3,b4
then a1,a4 // b1,b2 by A25, AFF_1:4;
then b1,b2 // b1,b4 by A8, A16, A26, AFF_1:5;
hence a3,a4 // b3,b4 by A5, A6, A7, A14, A18, A22, A24, A91, A90, AFF_1:14, AFF_1:25; :: thesis: verum

end;

A92: now :: thesis: ( a1 = a3 implies a3,a4 // b3,b4 )

o,b1 // o,b3 by A5, A7, A14, A15, AFF_1:39, AFF_1:41;
then A93: LIN o,b1,b3 by AFF_1:def 1;
assume A94: a1 = a3 ; :: thesis: a3,a4 // b3,b4
then a2,a1 // b2,b3 by A24, AFF_1:4;
then b2,b1 // b2,b3 by A8, A17, A25, AFF_1:5;
hence a3,a4 // b3,b4 by A4, A6, A7, A10, A18, A22, A26, A94, A93, AFF_1:14, AFF_1:25; :: thesis: verum

end;

assume ( a1 = a3 or a2 = a4 ) ; :: thesis: a3,a4 // b3,b4
hence a3,a4 // b3,b4 by A92, A89; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A27; :: thesis: verum

end;

hence X is satisfying_major_indirect_Scherungssatz ; :: thesis: verum

end;

( X is satisfying_major_indirect_Scherungssatz implies X is Pappian )

proof

assume A95: X is satisfying_major_indirect_Scherungssatz ; :: thesis: X is Pappian

now :: thesis: for M, N being Subset of X
for o, a, b, c, a1, b1, c1 being Element of X st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 holds
a,c1 // c,a1

let M, N be Subset of X; :: thesis: for o, a, b, c, a1, b1, c1 being Element of X st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 holds
a,c1 // c,a1
let o, a, b, c, a1, b1, c1 be Element of X; :: thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 implies a,c1 // c,a1 )
assume that
A96: M is being_line and
A97: N is being_line and
A98: M <> N and
A99: o in M and
A100: o in N and
A101: o <> a and
A102: o <> a1 and
A103: o <> b and
A104: o <> b1 and
A105: o <> c and
A106: o <> c1 and
A107: a in M and
A108: b in M and
A109: c in M and
A110: a1 in N and
A111: b1 in N and
A112: c1 in N and
A113: a,b1 // b,a1 and
A114: b,c1 // c,b1 ; :: thesis: a,c1 // c,a1
A115: ( not a in N & not b in N & not c in N & not a1 in M & not b1 in M & not c1 in M )

proof

A116: o,c1 // o,c1 by AFF_1:2;
A117: o,b1 // o,b1 by AFF_1:2;
A118: o,a1 // o,a1 by AFF_1:2;
A119: o,c // o,c by AFF_1:2;
A120: o,b // o,b by AFF_1:2;
A121: o,a // o,a by AFF_1:2;
assume ( a in N or b in N or c in N or a1 in M or b1 in M or c1 in M ) ; :: thesis: contradiction
then M // N by A96, A97, A99, A100, A101, A102, A103, A104, A105, A106, A107, A108, A109, A110, A111, A112, A121, A120, A119, A118, A117, A116, AFF_1:38;
hence contradiction by A98, A99, A100, AFF_1:45; :: thesis: verum

end;

A122: b,c1 // b1,c by A114, AFF_1:4;
A123: b1,b // b,b1 by AFF_1:2;
a,b1 // a1,b by A113, AFF_1:4;
then a,c1 // a1,c by A95, A96, A97, A99, A100, A107, A108, A109, A110, A111, A112, A115, A122, A123;
hence a,c1 // c,a1 by AFF_1:4; :: thesis: verum

end;

hence X is Pappian by AFF_2:def 2; :: thesis: verum

end;

hence ( X is Pappian iff X is satisfying_major_indirect_Scherungssatz ) by A1; :: thesis: verum