let X be OrtAfPl; ( X is satisfying_MH2 implies X is satisfying_OSCH )
assume A1:
X is satisfying_MH2
; X is satisfying_OSCH
let a1 be Element of X; CONMETR:def 7 for a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & 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; for M, N being Subset of X st M _|_ N & 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; ( M _|_ N & 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
A2:
M _|_ N
and
A3:
a1 in M
and
A4:
a3 in M
and
A5:
b1 in M
and
A6:
b3 in M
and
A7:
a2 in N
and
A8:
a4 in N
and
A9:
b2 in N
and
A10:
b4 in N
and
A11:
not a4 in M
and
A12:
not a2 in M
and
A13:
not b2 in M
and
A14:
not b4 in M
and
A15:
not a1 in N
and
A16:
not a3 in N
and
A17:
not b1 in N
and
not b3 in N
and
A18:
a3,a2 // b3,b2
and
A19:
a2,a1 // b2,b1
and
A20:
a1,a4 // b1,b4
; a3,a4 // b3,b4
reconsider M9 = M, N9 = N as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;
N is being_line
by A2, ANALMETR:44;
then A21:
N9 is being_line
by ANALMETR:43;
reconsider b49 = b4, b19 = b1, b29 = b2, b39 = b3, a19 = a1, a29 = a2, a39 = a3, a49 = a4 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
M is being_line
by A2, ANALMETR:44;
then A22:
M9 is being_line
by ANALMETR:43;
not M9 // N9
then
ex o9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st
( o9 in M9 & o9 in N9 )
by A22, A21, AFF_1:58;
then consider o being Element of X such that
A23:
o in M
and
A24:
o in N
;
reconsider o9 = o as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
A25:
now ( b2 <> b4 implies a3,a4 // b3,b4 )assume A26:
b2 <> b4
;
a3,a4 // b3,b4A27:
now ( b1 <> b3 implies a3,a4 // b3,b4 )
ex
d39 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) st
(
o9 <> d39 &
d39 in N9 )
by A21, AFF_1:20;
then consider d3 being
Element of
X such that A28:
d3 in N
and A29:
d3 <> o
;
reconsider d39 =
d3 as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
consider e2 being
Element of
X such that A30:
a3,
a2 _|_ d3,
e2
and A31:
d3 <> e2
by ANALMETR:def 9;
consider e1 being
Element of
X such that A32:
a3,
a1 // a3,
e1
and A33:
a3 <> e1
by ANALMETR:39;
reconsider e19 =
e1,
e29 =
e2 as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
assume A34:
b1 <> b3
;
a3,a4 // b3,b4A35:
(
a1 <> a3 &
a2 <> a4 )
proof
assume
(
a1 = a3 or
a2 = a4 )
;
contradiction
then
(
a2,
a1 // b3,
b2 or
a1,
a4 // b2,
b1 )
by A18, A19, ANALMETR:59;
then
(
b3,
b2 // b2,
b1 or
b2,
b1 // b1,
b4 )
by A3, A11, A12, A19, A20, ANALMETR:60;
then
(
b2,
b3 // b2,
b1 or
b1,
b2 // b1,
b4 )
by ANALMETR:59;
then
(
LIN b2,
b3,
b1 or
LIN b1,
b2,
b4 )
by ANALMETR:def 10;
then
(
LIN b29,
b39,
b19 or
LIN b19,
b29,
b49 )
by ANALMETR:40;
then
(
LIN b19,
b39,
b29 or
LIN b29,
b49,
b19 )
by AFF_1:6;
hence
contradiction
by A5, A6, A9, A10, A13, A17, A22, A21, A26, A34, AFF_1:25;
verum
end;
not
a39,
e19 // d39,
e29
proof
assume
a39,
e19 // d39,
e29
;
contradiction
then
a3,
e1 // d3,
e2
by ANALMETR:36;
then
a3,
a1 // d3,
e2
by A32, A33, ANALMETR:60;
then A36:
a3,
a2 _|_ a3,
a1
by A30, A31, ANALMETR:62;
a3,
a1 _|_ a2,
a4
by A2, A3, A4, A7, A8, ANALMETR:56;
then
a3,
a2 // a2,
a4
by A35, A36, ANALMETR:63;
then
a2,
a4 // a2,
a3
by ANALMETR:59;
then
LIN a2,
a4,
a3
by ANALMETR:def 10;
then
LIN a29,
a49,
a39
by ANALMETR:40;
hence
contradiction
by A7, A8, A16, A21, A35, AFF_1:25;
verum
end; then consider d29 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A37:
LIN a39,
e19,
d29
and A38:
LIN d39,
e29,
d29
by AFF_1:60;
reconsider d2 =
d29 as
Element of
X ;
LIN d3,
e2,
d2
by A38, ANALMETR:40;
then
d3,
e2 // d3,
d2
by ANALMETR:def 10;
then A39:
a3,
a2 _|_ d3,
d2
by A30, A31, ANALMETR:62;
LIN a3,
e1,
d2
by A37, ANALMETR:40;
then
a3,
e1 // a3,
d2
by ANALMETR:def 10;
then
a3,
a1 // a3,
d2
by A32, A33, ANALMETR:60;
then
LIN a3,
a1,
d2
by ANALMETR:def 10;
then
LIN a39,
a19,
d29
by ANALMETR:40;
then consider d2 being
Element of
X such that A40:
d2 in M
and A41:
a3,
a2 _|_ d3,
d2
by A3, A4, A22, A35, A39, AFF_1:25;
reconsider d29 =
d2 as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
consider e1 being
Element of
X such that A42:
a2,
a4 // a2,
e1
and A43:
a2 <> e1
by ANALMETR:39;
consider e2 being
Element of
X such that A44:
a2,
a1 _|_ d2,
e2
and A45:
d2 <> e2
by ANALMETR:def 9;
reconsider e19 =
e1,
e29 =
e2 as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
not
a29,
e19 // d29,
e29
proof
assume
a29,
e19 // d29,
e29
;
contradiction
then
a2,
e1 // d2,
e2
by ANALMETR:36;
then
a2,
a4 // d2,
e2
by A42, A43, ANALMETR:60;
then A46:
a2,
a4 _|_ a2,
a1
by A44, A45, ANALMETR:62;
a1,
a3 _|_ a2,
a4
by A2, A3, A4, A7, A8, ANALMETR:56;
then
a1,
a3 // a2,
a1
by A35, A46, ANALMETR:63;
then
a1,
a3 // a1,
a2
by ANALMETR:59;
then
LIN a1,
a3,
a2
by ANALMETR:def 10;
then
LIN a19,
a39,
a29
by ANALMETR:40;
hence
contradiction
by A3, A4, A12, A22, A35, AFF_1:25;
verum
end; then consider d19 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A47:
LIN a29,
e19,
d19
and A48:
LIN d29,
e29,
d19
by AFF_1:60;
reconsider d1 =
d19 as
Element of
X ;
A49:
b3,
b2 _|_ d3,
d2
by A4, A12, A18, A41, ANALMETR:62;
LIN a2,
e1,
d1
by A47, ANALMETR:40;
then
a2,
e1 // a2,
d1
by ANALMETR:def 10;
then
a2,
a4 // a2,
d1
by A42, A43, ANALMETR:60;
then
LIN a2,
a4,
d1
by ANALMETR:def 10;
then
LIN a29,
a49,
d19
by ANALMETR:40;
then A50:
d1 in N
by A7, A8, A21, A35, AFF_1:25;
LIN d2,
e2,
d1
by A48, ANALMETR:40;
then
d2,
e2 // d2,
d1
by ANALMETR:def 10;
then A51:
a2,
a1 _|_ d2,
d1
by A44, A45, ANALMETR:62;
then A52:
b2,
b1 _|_ d2,
d1
by A3, A12, A19, ANALMETR:62;
consider e2 being
Element of
X such that A53:
a1,
a4 _|_ d1,
e2
and A54:
d1 <> e2
by ANALMETR:39;
consider e1 being
Element of
X such that A55:
a1,
a3 // a1,
e1
and A56:
a1 <> e1
by ANALMETR:39;
reconsider e19 =
e1,
e29 =
e2 as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
not
a19,
e19 // d19,
e29
proof
assume
a19,
e19 // d19,
e29
;
contradiction
then
a1,
e1 // d1,
e2
by ANALMETR:36;
then
a1,
a3 // d1,
e2
by A55, A56, ANALMETR:60;
then A57:
a1,
a3 _|_ a1,
a4
by A53, A54, ANALMETR:62;
a1,
a3 _|_ a2,
a4
by A2, A3, A4, A7, A8, ANALMETR:56;
then
a2,
a4 // a1,
a4
by A35, A57, ANALMETR:63;
then
a4,
a2 // a4,
a1
by ANALMETR:59;
then
LIN a4,
a2,
a1
by ANALMETR:def 10;
then
LIN a49,
a29,
a19
by ANALMETR:40;
hence
contradiction
by A7, A8, A15, A21, A35, AFF_1:25;
verum
end; then consider d49 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A58:
LIN a19,
e19,
d49
and A59:
LIN d19,
e29,
d49
by AFF_1:60;
reconsider d4 =
d49 as
Element of
X ;
LIN a1,
e1,
d4
by A58, ANALMETR:40;
then
a1,
e1 // a1,
d4
by ANALMETR:def 10;
then
a1,
a3 // a1,
d4
by A55, A56, ANALMETR:60;
then
LIN a1,
a3,
d4
by ANALMETR:def 10;
then
LIN a19,
a39,
d49
by ANALMETR:40;
then A60:
d4 in M
by A3, A4, A22, A35, AFF_1:25;
then A61:
d3 <> d4
by A2, A22, A21, A23, A24, A28, A29, AFF_1:18;
LIN d1,
e2,
d4
by A59, ANALMETR:40;
then
d1,
e2 // d1,
d4
by ANALMETR:def 10;
then A62:
a1,
a4 _|_ d1,
d4
by A53, A54, ANALMETR:62;
then
b1,
b4 _|_ d1,
d4
by A3, A11, A20, ANALMETR:62;
then A63:
b3,
b4 _|_ d3,
d4
by A1, A2, A5, A6, A9, A10, A13, A14, A28, A40, A50, A60, A49, A52;
a3,
a4 _|_ d3,
d4
by A1, A2, A3, A4, A7, A8, A11, A12, A28, A40, A41, A50, A51, A60, A62;
hence
a3,
a4 // b3,
b4
by A63, A61, ANALMETR:63;
verum now ( b1 = b3 implies a3,a4 // b3,b4 )
o9,
a19 // o9,
a39
by A3, A4, A22, A23, AFF_1:39, AFF_1:41;
then A64:
LIN o9,
a19,
a39
by AFF_1:def 1;
assume A65:
b1 = b3
;
a3,a4 // b3,b4then
a2,
a1 // b3,
b2
by A19, ANALMETR:59;
then
a2,
a1 // a3,
a2
by A6, A13, A18, ANALMETR:60;
then
a2,
a1 // a2,
a3
by ANALMETR:59;
then
a29,
a19 // a29,
a39
by ANALMETR:36;
hence
a3,
a4 // b3,
b4
by A7, A12, A15, A20, A21, A23, A24, A65, A64, AFF_1:14, AFF_1:25;
verum end; hence
a3,
a4 // b3,
b4
by A27;
verum end;
now ( b2 = b4 implies a3,a4 // b3,b4 )
o9,
a29 // o9,
a49
by A7, A8, A21, A24, AFF_1:39, AFF_1:41;
then A66:
LIN o9,
a29,
a49
by AFF_1:def 1;
assume A67:
b2 = b4
;
a3,a4 // b3,b4then
a1,
a4 // b2,
b1
by A20, ANALMETR:59;
then
a2,
a1 // a1,
a4
by A5, A13, A19, ANALMETR:60;
then
a1,
a2 // a1,
a4
by ANALMETR:59;
then
a19,
a29 // a19,
a49
by ANALMETR:36;
hence
a3,
a4 // b3,
b4
by A3, A12, A15, A18, A22, A23, A24, A67, A66, AFF_1:14, AFF_1:25;
verum end;
hence
a3,a4 // b3,b4
by A25; verum