let X be OrtAfPl; :: thesis: ( X is satisfying_LIN1 implies X is satisfying_LIN2 )
assume A1: X is satisfying_LIN1 ; :: thesis: X is satisfying_LIN2
let o be Element of X; :: according to CONAFFM:def 7 :: thesis: for a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & a,a1 // b,b1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 holds
o,c _|_ o,c1
let a, a1, b, b1, c, c1 be Element of X; :: thesis: ( o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & a,a1 // b,b1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 implies o,c _|_ o,c1 )
assume A2: ( o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & a,a1 // b,b1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 ) ; :: thesis: o,c _|_ o,c1
reconsider a' = a, a1' = a1, b' = b, b1' = b1, c' = c, c1' = c1, o' = o as Element of (Af X) by ANALMETR:47;
ex c2 being Element of X st
( LIN a1,c1,c2 & o,c _|_ o,c2 & o <> c2 )

proof

consider e1 being Element of X such that
A3: ( a1,c1 // a1,e1 & a1 <> e1 ) by ANALMETR:51;
consider e2 being Element of X such that
A4: ( o,c _|_ o,e2 & o <> e2 ) by ANALMETR:51;
reconsider e1' = e1, e2' = e2 as Element of (Af X) by ANALMETR:47;
not a1',e1' // o',e2'

proof

assume a1',e1' // o',e2' ; :: thesis: contradiction
then a1,e1 // o,e2 by ANALMETR:48;
then a1,c1 // o,e2 by A3, ANALMETR:82;
then A5: a1,c1 _|_ o,c by A4, ANALMETR:84;
a1 <> c1

proof

assume A6: a1 = c1 ; :: thesis: contradiction
A7: b1 <> a1

proof

assume b1 = a1 ; :: thesis: contradiction
then a1,a // a1,b by A2, ANALMETR:81;
then LIN a1,a,b by ANALMETR:def 11;
then LIN a1',a',b' by ANALMETR:55;
then LIN a',b',a1' by AFF_1:15;
then LIN a,b,a1 by ANALMETR:55;
then A8: a,b // a,a1 by ANALMETR:def 11;
o,a // a,b

proof

LIN o',a',b' by A2, ANALMETR:55;
then LIN a',b',o' by AFF_1:15;
then LIN a,b,o by ANALMETR:55;
then a,b // a,o by ANALMETR:def 11;
hence o,a // a,b by ANALMETR:81; :: thesis: verum

end;

then a,a1 // o,a by A2, A8, ANALMETR:82;
then a,a1 // a,o by ANALMETR:81;
then LIN a,a1,o by ANALMETR:def 11;
then LIN a',a1',o' by ANALMETR:55;
then LIN o',a',a1' by AFF_1:15;
then LIN o,a,a1 by ANALMETR:55;
then o,a // o,a1 by ANALMETR:def 11;
then o,a _|_ o,a by A2, ANALMETR:84;
hence contradiction by A2, ANALMETR:51; :: thesis: verum

end;

b1,a1 _|_ b,a

proof

( LIN o',a',b' & LIN o',a1',b1' ) by A2, ANALMETR:55;
then ( LIN b',o',a' & LIN b1',o',a1' ) by AFF_1:15;
then ( LIN b,o,a & LIN b1,o,a1 ) by ANALMETR:55;
then A9: ( b,o // b,a & b1,o // b1,a1 ) by ANALMETR:def 11;
b,o _|_ b1,o by A2, ANALMETR:83;
then b,a _|_ b1,o by A2, A9, ANALMETR:84;
hence b1,a1 _|_ b,a by A2, A9, ANALMETR:84; :: thesis: verum

end;

then b,c // b,a by A2, A6, A7, ANALMETR:85;
then LIN b,c,a by ANALMETR:def 11;
then LIN b',c',a' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
then LIN a,b,c by ANALMETR:55;
then A10: a,b // a,c by ANALMETR:def 11;
LIN o',a',b' by A2, ANALMETR:55;
then LIN a',b',o' by AFF_1:15;
then LIN a,b,o by ANALMETR:55;
then a,b // a,o by ANALMETR:def 11;
then a,c // a,o by A2, A10, ANALMETR:82;
then LIN a,c,o by ANALMETR:def 11;
then LIN a',c',o' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then a,c // o,c by A2, A5, ANALMETR:85;
then c,a // c,o by ANALMETR:81;
then c',a' // c',o' by ANALMETR:48;
then LIN c',a',o' by AFF_1:def 1;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then consider c2' being Element of (Af X) such that
A11: ( LIN a1',e1',c2' & LIN o',e2',c2' ) by AFF_1:74;
reconsider c2 = c2' as Element of X by ANALMETR:47;
take c2 ; :: thesis: ( LIN a1,c1,c2 & o,c _|_ o,c2 & o <> c2 )
a1',e1' // a1',c2' by A11, AFF_1:def 1;
then a1,e1 // a1,c2 by ANALMETR:48;
then A12: a1,c1 // a1,c2 by A3, ANALMETR:82;
LIN o,e2,c2 by A11, ANALMETR:55;
then A13: o,e2 // o,c2 by ANALMETR:def 11;
o <> c2

proof

assume o = c2 ; :: thesis: contradiction
then a1,c1 // o,a1 by A12, ANALMETR:81;
then A14: o,a _|_ a1,c1 by A2, ANALMETR:84;
a1 <> c1

proof

assume A15: a1 = c1 ; :: thesis: contradiction
A16: a1 <> b1

proof

assume a1 = b1 ; :: thesis: contradiction
then a1,a // a1,b by A2, ANALMETR:81;
then LIN a1,a,b by ANALMETR:def 11;
then LIN a1',a',b' by ANALMETR:55;
then LIN a',b',a1' by AFF_1:15;
then LIN a,b,a1 by ANALMETR:55;
then A17: a,b // a,a1 by ANALMETR:def 11;
o,a // a,b

proof

LIN o',a',b' by A2, ANALMETR:55;
then LIN a',b',o' by AFF_1:15;
then LIN a,b,o by ANALMETR:55;
then a,b // a,o by ANALMETR:def 11;
hence o,a // a,b by ANALMETR:81; :: thesis: verum

end;

then a,a1 // o,a by A2, A17, ANALMETR:82;
then a,a1 // a,o by ANALMETR:81;
then LIN a,a1,o by ANALMETR:def 11;
then LIN a',a1',o' by ANALMETR:55;
then LIN o',a',a1' by AFF_1:15;
then LIN o,a,a1 by ANALMETR:55;
then o,a // o,a1 by ANALMETR:def 11;
then o,a _|_ o,a by A2, ANALMETR:84;
hence contradiction by A2, ANALMETR:51; :: thesis: verum

end;

b1,a1 // o,b1

proof

LIN o',a1',b1' by A2, ANALMETR:55;
then LIN b1',a1',o' by AFF_1:15;
then LIN b1,a1,o by ANALMETR:55;
then b1,a1 // b1,o by ANALMETR:def 11;
hence b1,a1 // o,b1 by ANALMETR:81; :: thesis: verum

end;

then b,c _|_ o,b1 by A2, A15, A16, ANALMETR:84;
then A18: b,c // o,b by A2, ANALMETR:85;
LIN o',a',b' by A2, ANALMETR:55;
then ( LIN b',a',o' & LIN a',b',o' ) by AFF_1:15;
then ( LIN b,a,o & LIN a,b,o ) by ANALMETR:55;
then A19: ( b,a // b,o & a,b // a,o ) by ANALMETR:def 11;
then o,b // b,a by ANALMETR:81;
then b,a // b,c by A2, A18, ANALMETR:82;
then LIN b,a,c by ANALMETR:def 11;
then LIN b',a',c' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
then LIN a,b,c by ANALMETR:55;
then a,b // a,c by ANALMETR:def 11;
then a,o // a,c by A2, A19, ANALMETR:82;
then LIN a,o,c by ANALMETR:def 11;
then LIN a',o',c' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then o,a // a,c by A2, A14, ANALMETR:85;
then a,c // a,o by ANALMETR:81;
then LIN a,c,o by ANALMETR:def 11;
then LIN a',c',o' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

hence ( LIN a1,c1,c2 & o,c _|_ o,c2 & o <> c2 ) by A4, A12, A13, ANALMETR:84, ANALMETR:def 11; :: thesis: verum

end;

then consider c2 being Element of X such that
A20: ( LIN a1,c1,c2 & o,c _|_ o,c2 & o <> c2 ) ;
reconsider c2' = c2 as Element of (Af X) by ANALMETR:47;
A21: ( b <> c & a1 <> b1 & a1 <> c1 )

proof

assume A22: ( b = c or a1 = b1 or a1 = c1 ) ; :: thesis: contradiction

A23: now

assume b = c ; :: thesis: contradiction
then LIN o',a',c' by A2, ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

A24: now

assume a1 = b1 ; :: thesis: contradiction
then a1,a // a1,b by A2, ANALMETR:81;
then LIN a1,a,b by ANALMETR:def 11;
then LIN a1',a',b' by ANALMETR:55;
then LIN a',b',a1' by AFF_1:15;
then LIN a,b,a1 by ANALMETR:55;
then A25: a,b // a,a1 by ANALMETR:def 11;
o,a // a,b

proof

LIN o',a',b' by A2, ANALMETR:55;
then LIN a',b',o' by AFF_1:15;
then LIN a,b,o by ANALMETR:55;
then a,b // a,o by ANALMETR:def 11;
hence o,a // a,b by ANALMETR:81; :: thesis: verum

end;

then a,a1 // o,a by A2, A25, ANALMETR:82;
then a,a1 // a,o by ANALMETR:81;
then LIN a,a1,o by ANALMETR:def 11;
then LIN a',a1',o' by ANALMETR:55;
then LIN o',a',a1' by AFF_1:15;
then LIN o,a,a1 by ANALMETR:55;
then o,a // o,a1 by ANALMETR:def 11;
then o,a _|_ o,a by A2, ANALMETR:84;
hence contradiction by A2, ANALMETR:51; :: thesis: verum

end;

now

assume A26: a1 = c1 ; :: thesis: contradiction
b1,a1 // o,b1

proof

LIN o',a1',b1' by A2, ANALMETR:55;
then LIN b1',a1',o' by AFF_1:15;
then LIN b1,a1,o by ANALMETR:55;
then b1,a1 // b1,o by ANALMETR:def 11;
hence b1,a1 // o,b1 by ANALMETR:81; :: thesis: verum

end;

then b,c _|_ o,b1 by A2, A24, A26, ANALMETR:84;
then A27: b,c // o,b by A2, ANALMETR:85;
LIN o',a',b' by A2, ANALMETR:55;
then ( LIN b',a',o' & LIN a',b',o' ) by AFF_1:15;
then ( LIN b,a,o & LIN a,b,o ) by ANALMETR:55;
then A28: ( b,a // b,o & a,b // a,o ) by ANALMETR:def 11;
then o,b // b,a by ANALMETR:81;
then b,a // b,c by A2, A27, ANALMETR:82;
then LIN b,a,c by ANALMETR:def 11;
then LIN b',a',c' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
then LIN a,b,c by ANALMETR:55;
then a,b // a,c by ANALMETR:def 11;
then a,o // a,c by A2, A28, ANALMETR:82;
then LIN a,o,c by ANALMETR:def 11;
then LIN a',o',c' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

hence contradiction by A22, A23, A24; :: thesis: verum

end;

a,c _|_ a1,c2

proof

a1,c1 // a1,c2 by A20, ANALMETR:def 11;
hence a,c _|_ a1,c2 by A2, A21, ANALMETR:84; :: thesis: verum

end;

then b,c _|_ b1,c2 by A1, A2, A20, Def6;
then b1,c1 // b1,c2 by A2, A21, ANALMETR:85;
then A29: LIN b1,c1,c2 by ANALMETR:def 11;
c1 = c2

proof

not LIN b1,a1,c1

proof

assume LIN b1,a1,c1 ; :: thesis: contradiction
then LIN b1',a1',c1' by ANALMETR:55;
then LIN a1',b1',c1' by AFF_1:15;
then a1',b1' // a1',c1' by AFF_1:def 1;
then A30: a1,b1 // a1,c1 by ANALMETR:48;
LIN o',a1',b1' by A2, ANALMETR:55;
then LIN a1',b1',o' by AFF_1:15;
then LIN a1,b1,o by ANALMETR:55;
then a1,b1 // a1,o by ANALMETR:def 11;
then a1,c1 // a1,o by A21, A30, ANALMETR:82;
then a,c _|_ a1,o by A2, A21, ANALMETR:84;
then A31: o,a1 _|_ a,c by ANALMETR:83;
o,a1 _|_ a,o by A2, ANALMETR:83;
then a,o // a,c by A2, A31, ANALMETR:85;
then LIN a,o,c by ANALMETR:def 11;
then LIN a',o',c' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then A32: not LIN b1',a1',c1' by ANALMETR:55;
A33: LIN b1',c1',c2' by A29, ANALMETR:55;
a1,c1 // a1,c2 by A20, ANALMETR:def 11;
then a1',c1' // a1',c2' by ANALMETR:48;
hence c1 = c2 by A32, A33, AFF_1:23; :: thesis: verum

end;

hence o,c _|_ o,c1 by A20; :: thesis: verum