let X be OrtAfPl; :: thesis: ( X is satisfying_OSCH & X is satisfying_TDES implies X is satisfying_SCH )
assume that
A1: X is satisfying_OSCH and
A2: X is satisfying_TDES ; :: thesis: X is satisfying_SCH
let a1 be Element of X; :: according to CONMETR:def 6 :: thesis: for 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 & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4
let 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 & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 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 & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 )
assume that
A3: ( M is being_line & N is being_line ) and
A4: ( a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 ) ; :: thesis: a3,a4 // b3,b4
reconsider a1' = a1, a2' = a2, a3' = a3, a4' = a4, b1' = b1, b2' = b2, b3' = b3, b4' = b4 as Element of (Af X) by ANALMETR:47;
reconsider M' = M, N' = N as Subset of (Af X) by ANALMETR:57;
A5: ( M' is being_line & N' is being_line ) by A3, ANALMETR:58;
A6: ( a1 = b1 implies ( a2 = b2 & a3 = b3 & a4 = b4 ) )

proof

assume A7: a1 = b1 ; :: thesis: ( a2 = b2 & a3 = b3 & a4 = b4 )
assume A8: ( a2 <> b2 or a3 <> b3 or a4 <> b4 ) ; :: thesis: contradiction

A9: now

assume A10: a2 <> b2 ; :: thesis: contradiction
a1,a2 // a1,b2 by A4, A7, ANALMETR:81;
then LIN a1,a2,b2 by ANALMETR:def 11;
then LIN a1',a2',b2' by ANALMETR:55;
then LIN a2',b2',a1' by AFF_1:15;
hence contradiction by A4, A5, A10, AFF_1:39; :: thesis: verum

end;

A11: now

assume A12: a4 <> b4 ; :: thesis: contradiction
LIN a1,a4,b4 by A4, A7, ANALMETR:def 11;
then LIN a1',a4',b4' by ANALMETR:55;
then LIN a4',b4',a1' by AFF_1:15;
hence contradiction by A4, A5, A12, AFF_1:39; :: thesis: verum

end;

now

assume A13: a3 <> b3 ; :: thesis: contradiction
a2,a3 // a2,b3 by A4, A9, ANALMETR:81;
then LIN a2,a3,b3 by ANALMETR:def 11;
then LIN a2',a3',b3' by ANALMETR:55;
then LIN a3',b3',a2' by AFF_1:15;
hence contradiction by A4, A5, A13, AFF_1:39; :: thesis: verum

end;

hence contradiction by A8, A9, A11; :: thesis: verum

end;

A14: now

assume a1 = b1 ; :: thesis: a3,a4 // b3,b4
then a3',a4' // b3',b4' by A6, AFF_1:11;
hence a3,a4 // b3,b4 by ANALMETR:48; :: thesis: verum

end;

A15: ( a1 <> b1 implies ( a2 <> b2 & a3 <> b3 & a4 <> b4 ) )

proof

assume A16: a1 <> b1 ; :: thesis: ( a2 <> b2 & a3 <> b3 & a4 <> b4 )
assume A17: ( a2 = b2 or a3 = b3 or a4 = b4 ) ; :: thesis: contradiction

A18: now

assume a2 = b2 ; :: thesis: contradiction
then LIN a2,a1,b1 by A4, ANALMETR:def 11;
then LIN a2',a1',b1' by ANALMETR:55;
then LIN a1',b1',a2' by AFF_1:15;
hence contradiction by A4, A5, A16, AFF_1:39; :: thesis: verum

end;

A19: now

assume a4 = b4 ; :: thesis: contradiction
then a4,a1 // a4,b1 by A4, ANALMETR:81;
then LIN a4,a1,b1 by ANALMETR:def 11;
then LIN a4',a1',b1' by ANALMETR:55;
then LIN a1',b1',a4' by AFF_1:15;
hence contradiction by A4, A5, A16, AFF_1:39; :: thesis: verum

end;

now

assume a3 = b3 ; :: thesis: contradiction
then LIN a3,a2,b2 by A4, ANALMETR:def 11;
then LIN a3',a2',b2' by ANALMETR:55;
then LIN a2',b2',a3' by AFF_1:15;
hence contradiction by A4, A5, A18, AFF_1:39; :: thesis: verum

end;

hence contradiction by A17, A18, A19; :: thesis: verum

end;

now

assume A20: a1 <> b1 ; :: thesis: a3,a4 // b3,b4

A21: now

assume A22: a2 = a4 ; :: thesis: a3,a4 // b3,b4
A23: not LIN a2',b1',b2'

proof

assume LIN a2',b1',b2' ; :: thesis: contradiction
then LIN a2',b2',b1' by AFF_1:15;
hence contradiction by A4, A5, A15, A20, AFF_1:39; :: thesis: verum

end;

A24: LIN a2',b2',b4'

proof

N' // N' by A5, AFF_1:55;
then a2',b2' // a2',b4' by A4, AFF_1:53;
hence LIN a2',b2',b4' by AFF_1:def 1; :: thesis: verum

end;

b1',b2' // b1',b4'

proof

a2,a1 // b1,b4 by A4, A22, ANALMETR:81;
then b2,b1 // b1,b4 by A4, ANALMETR:82;
then b1,b2 // b1,b4 by ANALMETR:81;
hence b1',b2' // b1',b4' by ANALMETR:48; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A4, A22, A23, A24, AFF_1:23; :: thesis: verum

end;

A25: now

assume A26: a1 = a3 ; :: thesis: a3,a4 // b3,b4
A27: not LIN a1',b2',b1'

proof

assume LIN a1',b2',b1' ; :: thesis: contradiction
then LIN a1',b1',b2' by AFF_1:15;
hence contradiction by A4, A5, A20, AFF_1:39; :: thesis: verum

end;

A28: LIN a1',b1',b3'

proof

M' // M' by A5, AFF_1:55;
then a1',b1' // a1',b3' by A4, AFF_1:53;
hence LIN a1',b1',b3' by AFF_1:def 1; :: thesis: verum

end;

b2',b1' // b2',b3'

proof

a2,a1 // b2,b3 by A4, A26, ANALMETR:81;
then b2,b1 // b2,b3 by A4, ANALMETR:82;
hence b2',b1' // b2',b3' by ANALMETR:48; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A4, A26, A27, A28, AFF_1:23; :: thesis: verum

end;

now

assume A29: ( a2 <> a4 & a1 <> a3 ) ; :: thesis: a3,a4 // b3,b4

A30: now

assume A31: M // N ; :: thesis: a3,a4 // b3,b4
consider x being Element of X such that
A32: ( LIN a1,a2,x & a1 <> x & a2 <> x ) by A4, Th2;
reconsider x' = x as Element of (Af X) by ANALMETR:47;
consider e1 being Element of X such that
A33: ( b1,b2 // b1,e1 & b1 <> e1 ) by ANALMETR:51;
consider e2 being Element of X such that
A34: ( a1,b1 // x,e2 & x <> e2 ) by ANALMETR:51;
reconsider e1' = e1, e2' = e2 as Element of (Af X) by ANALMETR:47;
not b1',e1' // x',e2'

proof

assume b1',e1' // x',e2' ; :: thesis: contradiction
then b1,e1 // x,e2 by ANALMETR:48;
then b1,b2 // x,e2 by A33, ANALMETR:82;
then b1,b2 // a1,b1 by A34, ANALMETR:82;
then b1,a1 // b1,b2 by ANALMETR:81;
then LIN b1,a1,b2 by ANALMETR:def 11;
then LIN b1',a1',b2' by ANALMETR:55;
hence contradiction by A4, A5, A20, AFF_1:39; :: thesis: verum

end;

then consider y' being Element of (Af X) such that
A35: ( LIN b1',e1',y' & LIN x',e2',y' ) by AFF_1:74;
reconsider y = y' as Element of X by ANALMETR:47;
A36: LIN b1,b2,y

proof

LIN b1,e1,y by A35, ANALMETR:55;
then b1,e1 // b1,y by ANALMETR:def 11;
then b1,b2 // b1,y by A33, ANALMETR:82;
hence LIN b1,b2,y by ANALMETR:def 11; :: thesis: verum

end;

A37: a1,b1 // x,y

proof

LIN x,e2,y by A35, ANALMETR:55;
then x,e2 // x,y by ANALMETR:def 11;
hence a1,b1 // x,y by A34, ANALMETR:82; :: thesis: verum

end;

A38: ( X is satisfying_TDES implies X is satisfying_des )

proof

assume X is satisfying_TDES ; :: thesis: X is satisfying_des
then Af X is Moufangian by Th7;
then Af X is translational by AFF_2:28;
hence X is satisfying_des by Th8; :: thesis: verum

end;

A39: not LIN a1,b1,x

proof

assume LIN a1,b1,x ; :: thesis: contradiction
then LIN a1',b1',x' by ANALMETR:55;
then A40: x' in M' by A4, A5, A20, AFF_1:39;
LIN a1',a2',x' by A32, ANALMETR:55;
then LIN a1',x',a2' by AFF_1:15;
hence contradiction by A4, A5, A32, A40, AFF_1:39; :: thesis: verum

end;

A41: not LIN a1,b1,a4

proof

assume LIN a1,b1,a4 ; :: thesis: contradiction
then LIN a1',b1',a4' by ANALMETR:55;
hence contradiction by A4, A5, A20, AFF_1:39; :: thesis: verum

end;

A42: a1,b1 // a4,b4

proof

M' // N' by A31, ANALMETR:64;
then a1',b1' // a4',b4' by A4, AFF_1:53;
hence a1,b1 // a4,b4 by ANALMETR:48; :: thesis: verum

end;

A43: a1,x // b1,y

proof

A44: b1,b2 // b1,y by A36, ANALMETR:def 11;
a1,a2 // b1,b2 by A4, ANALMETR:81;
then A45: a1,a2 // b1,y by A4, A44, ANALMETR:82;
a1,a2 // a1,x by A32, ANALMETR:def 11;
hence a1,x // b1,y by A4, A45, ANALMETR:82; :: thesis: verum

end;

then A46: x,a4 // y,b4 by A2, A4, A37, A38, A39, A41, A42, Def8;
A47: not LIN a2,b2,x

proof

assume LIN a2,b2,x ; :: thesis: contradiction
then A48: LIN a2',b2',x' by ANALMETR:55;
a2 <> b2

proof

assume a2 = b2 ; :: thesis: contradiction
then LIN a2,a1,b1 by A4, ANALMETR:def 11;
then LIN a2',a1',b1' by ANALMETR:55;
then LIN a1',b1',a2' by AFF_1:15;
hence contradiction by A4, A5, A20, AFF_1:39; :: thesis: verum

end;

then A49: x' in N' by A4, A5, A48, AFF_1:39;
LIN a1',a2',x' by A32, ANALMETR:55;
then LIN a2',x',a1' by AFF_1:15;
hence contradiction by A4, A5, A32, A49, AFF_1:39; :: thesis: verum

end;

A50: not LIN a2,b2,a3

proof

assume LIN a2,b2,a3 ; :: thesis: contradiction
then A51: LIN a2',b2',a3' by ANALMETR:55;
a2 <> b2

proof

assume a2 = b2 ; :: thesis: contradiction
then LIN a2,a1,b1 by A4, ANALMETR:def 11;
then LIN a2',a1',b1' by ANALMETR:55;
then LIN a1',b1',a2' by AFF_1:15;
hence contradiction by A4, A5, A20, AFF_1:39; :: thesis: verum

end;

hence contradiction by A4, A5, A51, AFF_1:39; :: thesis: verum

end;

A52: a2,b2 // x,y

proof

M' // N' by A31, ANALMETR:64;
then a1',b1' // a2',b2' by A4, AFF_1:53;
then a1,b1 // a2,b2 by ANALMETR:48;
hence a2,b2 // x,y by A20, A37, ANALMETR:82; :: thesis: verum

end;

A53: a2,b2 // a3,b3

proof

M' // N' by A31, ANALMETR:64;
then a3',b3' // a2',b2' by A4, AFF_1:53;
then a3,b3 // a2,b2 by ANALMETR:48;
hence a2,b2 // a3,b3 by ANALMETR:81; :: thesis: verum

end;

A54: a2,x // b2,y

proof

LIN a1',a2',x' by A32, ANALMETR:55;
then LIN x',a1',a2' by AFF_1:15;
then LIN x,a1,a2 by ANALMETR:55;
then x,a1 // x,a2 by ANALMETR:def 11;
then a1,x // a2,x by ANALMETR:81;
then A55: a2,x // b1,y by A32, A43, ANALMETR:82;
A56: b1 <> y

proof

assume b1 = y ; :: thesis: contradiction
then b1,a1 // b1,x by A37, ANALMETR:81;
then LIN b1,a1,x by ANALMETR:def 11;
then LIN b1',a1',x' by ANALMETR:55;
then A57: x' in M' by A4, A5, A20, AFF_1:39;
LIN a1',a2',x' by A32, ANALMETR:55;
then LIN a1',x',a2' by AFF_1:15;
hence contradiction by A4, A5, A32, A57, AFF_1:39; :: thesis: verum

end;

LIN b1',b2',y' by A36, ANALMETR:55;
then LIN y',b1',b2' by AFF_1:15;
then LIN y,b1,b2 by ANALMETR:55;
then y,b1 // y,b2 by ANALMETR:def 11;
then b1,y // b2,y by ANALMETR:81;
hence a2,x // b2,y by A55, A56, ANALMETR:82; :: thesis: verum

end;

a2,a3 // b2,b3 by A4, ANALMETR:81;
then A58: x,a3 // y,b3 by A2, A38, A47, A50, A52, A53, A54, Def8;
A59: not LIN x,y,a3

proof

assume LIN x,y,a3 ; :: thesis: contradiction
then A60: x,y // x,a3 by ANALMETR:def 11;
A61: x <> y

proof

assume x = y ; :: thesis: contradiction
then x,a1 // x,b1 by A43, ANALMETR:81;
then LIN x,a1,b1 by ANALMETR:def 11;
then LIN x',a1',b1' by ANALMETR:55;
then LIN a1',b1',x' by AFF_1:15;
then A62: x' in M' by A4, A5, A20, AFF_1:39;
LIN a1',a2',x' by A32, ANALMETR:55;
then LIN x',a1',a2' by AFF_1:15;
hence contradiction by A4, A5, A32, A62, AFF_1:39; :: thesis: verum

end;

M' // M' by A5, AFF_1:55;
then a1',a3' // a1',b1' by A4, AFF_1:53;
then a1,a3 // a1,b1 by ANALMETR:48;
then x,y // a1,a3 by A20, A37, ANALMETR:82;
then x,a3 // a1,a3 by A60, A61, ANALMETR:82;
then a3,a1 // a3,x by ANALMETR:81;
then LIN a3,a1,x by ANALMETR:def 11;
then LIN a3',a1',x' by ANALMETR:55;
then A63: x' in M' by A4, A5, A29, AFF_1:39;
LIN a1',a2',x' by A32, ANALMETR:55;
then LIN a1',x',a2' by AFF_1:15;
hence contradiction by A4, A5, A32, A63, AFF_1:39; :: thesis: verum

end;

A64: not LIN x,y,a4

proof

assume LIN x,y,a4 ; :: thesis: contradiction
then A65: x,y // x,a4 by ANALMETR:def 11;
A66: x <> y

proof

assume x = y ; :: thesis: contradiction
then x,a1 // x,b1 by A43, ANALMETR:81;
then LIN x,a1,b1 by ANALMETR:def 11;
then LIN x',a1',b1' by ANALMETR:55;
then LIN a1',b1',x' by AFF_1:15;
then A67: x' in M' by A4, A5, A20, AFF_1:39;
LIN a1',a2',x' by A32, ANALMETR:55;
then LIN x',a1',a2' by AFF_1:15;
hence contradiction by A4, A5, A32, A67, AFF_1:39; :: thesis: verum

end;

M' // N' by A31, ANALMETR:64;
then a1',b1' // a2',a4' by A4, AFF_1:53;
then a1,b1 // a2,a4 by ANALMETR:48;
then a2,a4 // x,y by A20, A37, ANALMETR:82;
then a2,a4 // x,a4 by A65, A66, ANALMETR:82;
then a4,a2 // a4,x by ANALMETR:81;
then LIN a4,a2,x by ANALMETR:def 11;
then LIN a4',a2',x' by ANALMETR:55;
then A68: x' in N' by A4, A5, A29, AFF_1:39;
LIN a1',a2',x' by A32, ANALMETR:55;
then LIN a2',x',a1' by AFF_1:15;
hence contradiction by A4, A5, A32, A68, AFF_1:39; :: thesis: verum

end;

A69: x,y // a3,b3

proof

M' // M' by A5, AFF_1:55;
then a1',b1' // a3',b3' by A4, AFF_1:53;
then a1,b1 // a3,b3 by ANALMETR:48;
hence x,y // a3,b3 by A20, A37, ANALMETR:82; :: thesis: verum

end;

x,y // a4,b4

proof

M' // N' by A31, ANALMETR:64;
then a1',b1' // a4',b4' by A4, AFF_1:53;
then a1,b1 // a4,b4 by ANALMETR:48;
hence x,y // a4,b4 by A20, A37, ANALMETR:82; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A2, A38, A46, A58, A59, A64, A69, Def8; :: thesis: verum

end;

now

assume not M // N ; :: thesis: a3,a4 // b3,b4
then not M' // N' by ANALMETR:64;
then consider o' being Element of (Af X) such that
A70: ( o' in M' & o' in N' ) by A5, AFF_1:72;
reconsider o = o' as Element of X by ANALMETR:47;
consider K being Subset of X such that
A71: ( o in K & N _|_ K ) by A3, Th3;
reconsider K' = K as Subset of (Af X) by ANALMETR:57;
A72: K is being_line by A71, ANALMETR:62;
then A73: ( K' is being_line & N' is being_line ) by A3, ANALMETR:58;

now

assume A74: K <> M ; :: thesis: a3,a4 // b3,b4

A75: now

let x' be Element of (Af X); :: thesis: ex y' being Element of (Af X) st
( y' in K' & x',y' // N' )
consider D' being Subset of (Af X) such that
A76: ( x' in D' & N' // D' ) by A5, AFF_1:63;
reconsider D = D' as Subset of the carrier of X by ANALMETR:57;
N // D by A76, ANALMETR:64;
then K _|_ D by A71, ANALMETR:73;
then consider y being Element of X such that
A77: ( y in K & y in D ) by ANALMETR:88;
reconsider y' = y as Element of (Af X) by ANALMETR:47;
take y' = y'; :: thesis: ( y' in K' & x',y' // N' )
thus ( y' in K' & x',y' // N' ) by A76, A77, AFF_1:54; :: thesis: verum

end;

then consider d1' being Element of (Af X) such that
A78: ( d1' in K' & a1',d1' // N' ) ;
consider d3' being Element of (Af X) such that
A79: ( d3' in K' & a3',d3' // N' ) by A75;
consider e3' being Element of (Af X) such that
A80: ( e3' in K' & b3',e3' // N' ) by A75;
consider e1' being Element of (Af X) such that
A81: ( e1' in K' & b1',e1' // N' ) by A75;
reconsider d1 = d1', d3 = d3', e1 = e1', e3 = e3' as Element of X by ANALMETR:47;
A82: ( o <> e1 & o <> e3 & o <> d1 & o <> d3 )

proof

assume A83: ( not o <> e1 or not o <> e3 or not o <> d1 or not o <> d3 ) ; :: thesis: contradiction

now

let x, y be Element of X; :: thesis: for x', y' being Element of the carrier of (Af X) st x',y' // N' & x = x' & y = y' & x in M & y in K & not x in N holds
not o = y
let x', y' be Element of the carrier of (Af X); :: thesis: ( x',y' // N' & x = x' & y = y' & x in M & y in K & not x in N implies not o = y )
assume that
A84: x',y' // N' and
A85: ( x = x' & y = y' ) and
A86: ( x in M & y in K & not x in N ) ; :: thesis: not o = y
assume o = y ; :: thesis: contradiction
then o',x' // N' by A84, A85, AFF_1:48;
hence contradiction by A5, A70, A85, A86, AFF_1:37; :: thesis: verum

end;

hence contradiction by A4, A78, A79, A80, A81, A83; :: thesis: verum

end;

A87: ( LIN o,a2,b2 & LIN o,a1,b1 & LIN o,a4,b4 & LIN o,a3,b3 ) by A3, A4, A70, Th4;
A88: ( LIN o,d1,e1 & LIN o,d3,e3 ) by A71, A72, A78, A79, A80, A81, Th4;
A89: ( not LIN a1,b1,d1 & not LIN a1,b1,a2 & not LIN a1,b1,a4 & not LIN a3,b3,d3 & not LIN a3,b3,a2 )

proof

A90: now

assume LIN a1,b1,d1 ; :: thesis: contradiction
then LIN a1',b1',d1' by ANALMETR:55;
then d1 in M by A4, A5, A20, AFF_1:39;
hence contradiction by A3, A70, A71, A72, A74, A78, A82, Th5; :: thesis: verum

end;

A91: now

assume LIN a1,b1,a2 ; :: thesis: contradiction
then LIN a1',b1',a2' by ANALMETR:55;
hence contradiction by A4, A5, A20, AFF_1:39; :: thesis: verum

end;

A92: now

assume LIN a1,b1,a4 ; :: thesis: contradiction
then LIN a1',b1',a4' by ANALMETR:55;
hence contradiction by A4, A5, A20, AFF_1:39; :: thesis: verum

end;

A93: now

assume LIN a3,b3,d3 ; :: thesis: contradiction
then LIN a3',b3',d3' by ANALMETR:55;
then d3 in M by A4, A5, A15, A20, AFF_1:39;
hence contradiction by A3, A70, A71, A72, A74, A79, A82, Th5; :: thesis: verum

end;

now

assume LIN a3,b3,a2 ; :: thesis: contradiction
then LIN a3',b3',a2' by ANALMETR:55;
hence contradiction by A4, A5, A15, A20, AFF_1:39; :: thesis: verum

end;

hence ( not LIN a1,b1,d1 & not LIN a1,b1,a2 & not LIN a1,b1,a4 & not LIN a3,b3,d3 & not LIN a3,b3,a2 ) by A90, A91, A92, A93; :: thesis: verum

end;

A94: d1,a1 // e1,b1

proof

a1',d1' // b1',e1' by A5, A78, A81, AFF_1:45;
then a1,d1 // b1,e1 by ANALMETR:48;
hence d1,a1 // e1,b1 by ANALMETR:81; :: thesis: verum

end;

A95: d1,a1 // o,a2

proof

a1,d1 // o,a2 by A4, A70, A78, Th6;
hence d1,a1 // o,a2 by ANALMETR:81; :: thesis: verum

end;

a1,a2 // b1,b2 by A4, ANALMETR:81;
then d1,a2 // e1,b2 by A2, A4, A70, A82, A87, A88, A89, A94, A95, Def5;
then A96: a2,d1 // b2,e1 by ANALMETR:81;
d1,a1 // o,a4

proof

a1,d1 // o,a4 by A4, A70, A78, Th6;
hence d1,a1 // o,a4 by ANALMETR:81; :: thesis: verum

end;

then A97: d1,a4 // e1,b4 by A2, A4, A70, A82, A87, A88, A89, A94, Def5;
A98: d3,a3 // e3,b3

proof

a3',d3' // b3',e3' by A5, A79, A80, AFF_1:45;
then a3,d3 // b3,e3 by ANALMETR:48;
hence d3,a3 // e3,b3 by ANALMETR:81; :: thesis: verum

end;

d3,a3 // o,a2

proof

a3,d3 // o,a2 by A4, A70, A79, Th6;
hence d3,a3 // o,a2 by ANALMETR:81; :: thesis: verum

end;

then A99: d3,a2 // e3,b2 by A2, A4, A70, A82, A87, A88, A89, A98, Def5;
A100: ( not d1 in N & not d3 in N & not e1 in N & not e3 in N ) by A4, A78, A79, A80, A81, AFF_1:49;
( not a2 in K & not a4 in K & not b2 in K & not b4 in K )

proof

A101: now

let x be Element of X; :: thesis: ( x in N & o <> x implies not x in K )
assume A102: ( x in N & o <> x ) ; :: thesis: not x in K
assume x in K ; :: thesis: contradiction
then o,x _|_ o,x by A70, A71, A102, ANALMETR:78;
hence contradiction by A102, ANALMETR:51; :: thesis: verum

end;

assume ( a2 in K or a4 in K or b2 in K or b4 in K ) ; :: thesis: contradiction
hence contradiction by A4, A70, A101; :: thesis: verum

end;

then A103: d3,a4 // e3,b4 by A1, A4, A71, A78, A79, A80, A81, A96, A97, A99, A100, Def7;
A104: ( not LIN d3,e3,a3 & not LIN d3,e3,a4 )

proof

A105: d3 <> e3

proof

assume not d3 <> e3 ; :: thesis: contradiction
then LIN e3,a3,b3 by A98, ANALMETR:def 11;
then LIN e3',a3',b3' by ANALMETR:55;
then LIN a3',b3',e3' by AFF_1:15;
then e3' in M' by A4, A5, A15, A20, AFF_1:39;
hence contradiction by A5, A70, A71, A73, A74, A80, A82, AFF_1:30; :: thesis: verum

end;

assume ( LIN d3,e3,a3 or LIN d3,e3,a4 ) ; :: thesis: contradiction
then ( LIN d3',e3',a3' or LIN d3',e3',a4' ) by ANALMETR:55;
then ( a3' in K' or a4' in K' ) by A73, A79, A80, A105, AFF_1:39;
hence contradiction by A4, A5, A70, A71, A73, A74, AFF_1:30; :: thesis: verum

end;

A106: a3,d3 // b3,e3 by A98, ANALMETR:81;
a3,d3 // o,a4 by A4, A70, A79, Th6;
hence a3,a4 // b3,b4 by A2, A4, A70, A82, A87, A88, A103, A104, A106, Def5; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A1, A4, A71, Def7; :: thesis: verum

end;

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

end;

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

end;

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