let X be OrtAfPl; :: thesis: ( X is satisfying_MH1 implies X is satisfying_OSCH )
assume A1:
X is satisfying_MH1
; :: thesis: X is satisfying_OSCH
let a1 be Element of X; :: according to CONMETR:def 7 :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: a3,a4 // b3,b4
reconsider M' = M, N' = N as Subset of (Af X) by ANALMETR:57;
N is being_line
by A2, ANALMETR:62;
then A21:
N' is being_line
by ANALMETR:58;
reconsider b4' = b4, b1' = b1, b2' = b2, b3' = b3, a1' = a1, a2' = a2, a3' = a3, a4' = a4 as Element of (Af X) by ANALMETR:47;
M is being_line
by A2, ANALMETR:62;
then A22:
M' is being_line
by ANALMETR:58;
not M' // N'
then
ex o' being Element of (Af X) st
( o' in M' & o' in N' )
by A22, A21, AFF_1:72;
then consider o being Element of X such that
A23:
o in M
and
A24:
o in N
;
reconsider o' = o as Element of (Af X) by ANALMETR:47;
A25:
now assume A26:
b2 <> b4
;
:: thesis: a3,a4 // b3,b4A27:
now consider e1' being
Element of
(Af X) such that A28:
o' <> e1'
and A29:
e1' in M'
by A22, AFF_1:32;
reconsider e1 =
e1' as
Element of
X by ANALMETR:47;
ex
d4' being
Element of
(Af X) st
(
o' <> d4' &
d4' in N' )
by A21, AFF_1:32;
then consider d4 being
Element of
X such that A30:
d4 in N
and A31:
d4 <> o
;
reconsider d4' =
d4 as
Element of
(Af X) by ANALMETR:47;
consider e2 being
Element of
X such that A32:
a1,
a4 _|_ d4,
e2
and A33:
e2 <> d4
by ANALMETR:51;
reconsider e2' =
e2 as
Element of
(Af X) by ANALMETR:47;
assume A34:
b1 <> b3
;
:: thesis: a3,a4 // b3,b4
not
o',
e1' // d4',
e2'
proof
A35:
a4' <> a2'
proof
assume
a4' = a2'
;
:: thesis: contradiction
then
a2,
a1 // b1,
b4
by A20, ANALMETR:81;
then
b1,
b4 // b2,
b1
by A3, A12, A19, ANALMETR:82;
then
b1,
b4 // b1,
b2
by ANALMETR:81;
then
LIN b1,
b4,
b2
by ANALMETR:def 11;
then
LIN b1',
b4',
b2'
by ANALMETR:55;
then
LIN b2',
b4',
b1'
by AFF_1:15;
hence
contradiction
by A9, A10, A17, A21, A26, AFF_1:39;
:: thesis: verum
end;
A36:
a1 <> a3
proof
assume
a1 = a3
;
:: thesis: contradiction
then
a3,
a2 // b2,
b1
by A19, ANALMETR:81;
then
b3,
b2 // b2,
b1
by A4, A12, A18, ANALMETR:82;
then
b2,
b3 // b2,
b1
by ANALMETR:81;
then
LIN b2,
b3,
b1
by ANALMETR:def 11;
then
LIN b2',
b3',
b1'
by ANALMETR:55;
then
LIN b1',
b3',
b2'
by AFF_1:15;
hence
contradiction
by A5, A6, A13, A22, A34, AFF_1:39;
:: thesis: verum
end;
assume
o',
e1' // d4',
e2'
;
:: thesis: contradiction
then
o,
e1 // d4,
e2
by ANALMETR:48;
then A37:
o,
e1 _|_ a1,
a4
by A32, A33, ANALMETR:84;
o',
e1' // a1',
a3'
by A3, A4, A22, A23, A29, AFF_1:53, AFF_1:55;
then
o,
e1 // a1,
a3
by ANALMETR:48;
then A38:
a1,
a3 _|_ a1,
a4
by A28, A37, ANALMETR:84;
a1,
a3 _|_ a2,
a4
by A2, A3, A4, A7, A8, ANALMETR:78;
then
a1,
a4 // a2,
a4
by A38, A36, ANALMETR:85;
then
a4,
a2 // a4,
a1
by ANALMETR:81;
then
LIN a4,
a2,
a1
by ANALMETR:def 11;
then
LIN a4',
a2',
a1'
by ANALMETR:55;
hence
contradiction
by A7, A8, A15, A21, A35, AFF_1:39;
:: thesis: verum
end; then consider d1' being
Element of
(Af X) such that A39:
LIN o',
e1',
d1'
and A40:
LIN d4',
e2',
d1'
by AFF_1:74;
reconsider d1 =
d1' as
Element of
X by ANALMETR:47;
consider e1' being
Element of
(Af X) such that A41:
o' <> e1'
and A42:
e1' in N'
by A21, AFF_1:32;
A43:
d1 in M
by A22, A23, A28, A29, A39, AFF_1:39;
LIN d4,
e2,
d1
by A40, ANALMETR:55;
then
d4,
e2 // d4,
d1
by ANALMETR:def 11;
then A44:
d1,
d4 // d4,
e2
by ANALMETR:81;
then
a1,
a4 _|_ d1,
d4
by A32, A33, ANALMETR:84;
then A45:
b1,
b4 _|_ d1,
d4
by A3, A11, A20, ANALMETR:84;
reconsider e1 =
e1' as
Element of
X by ANALMETR:47;
consider e2 being
Element of
X such that A46:
a2,
a1 _|_ d1,
e2
and A47:
e2 <> d1
by ANALMETR:51;
reconsider e2' =
e2 as
Element of
(Af X) by ANALMETR:47;
not
o',
e1' // e2',
d1'
proof
A48:
a1' <> a3'
proof
assume
a1' = a3'
;
:: thesis: contradiction
then
a3,
a2 // b2,
b1
by A19, ANALMETR:81;
then
b3,
b2 // b2,
b1
by A4, A12, A18, ANALMETR:82;
then
b2,
b3 // b2,
b1
by ANALMETR:81;
then
LIN b2,
b3,
b1
by ANALMETR:def 11;
then
LIN b2',
b3',
b1'
by ANALMETR:55;
then
LIN b1',
b3',
b2'
by AFF_1:15;
hence
contradiction
by A5, A6, A13, A22, A34, AFF_1:39;
:: thesis: verum
end;
o',
e1' // a2',
a4'
by A7, A8, A21, A24, A42, AFF_1:53, AFF_1:55;
then A49:
o,
e1 // a2,
a4
by ANALMETR:48;
A50:
a2 <> a4
proof
assume
a2 = a4
;
:: thesis: contradiction
then
a2,
a1 // b1,
b4
by A20, ANALMETR:81;
then
b1,
b4 // b2,
b1
by A3, A12, A19, ANALMETR:82;
then
b1,
b4 // b1,
b2
by ANALMETR:81;
then
LIN b1,
b4,
b2
by ANALMETR:def 11;
then
LIN b1',
b4',
b2'
by ANALMETR:55;
then
LIN b2',
b4',
b1'
by AFF_1:15;
hence
contradiction
by A9, A10, A17, A21, A26, AFF_1:39;
:: thesis: verum
end;
assume
o',
e1' // e2',
d1'
;
:: thesis: contradiction
then A51:
o,
e1 // e2,
d1
by ANALMETR:48;
a2,
a1 _|_ e2,
d1
by A46, ANALMETR:83;
then
o,
e1 _|_ a2,
a1
by A47, A51, ANALMETR:84;
then A52:
a2,
a1 _|_ a2,
a4
by A41, A49, ANALMETR:84;
a3,
a1 _|_ a2,
a4
by A2, A3, A4, A7, A8, ANALMETR:78;
then
a3,
a1 // a2,
a1
by A52, A50, ANALMETR:85;
then
a1,
a3 // a1,
a2
by ANALMETR:81;
then
LIN a1,
a3,
a2
by ANALMETR:def 11;
then
LIN a1',
a3',
a2'
by ANALMETR:55;
hence
contradiction
by A3, A4, A12, A22, A48, AFF_1:39;
:: thesis: verum
end; then consider d2' being
Element of
(Af X) such that A53:
LIN o',
e1',
d2'
and A54:
LIN e2',
d1',
d2'
by AFF_1:74;
reconsider d2 =
d2' as
Element of
X by ANALMETR:47;
A55:
d2 in N
by A21, A24, A41, A42, A53, AFF_1:39;
LIN d1',
d2',
e2'
by A54, AFF_1:15;
then
LIN d1,
d2,
e2
by ANALMETR:55;
then
d1,
d2 // d1,
e2
by ANALMETR:def 11;
then A56:
d2,
d1 // e2,
d1
by ANALMETR:81;
A57:
a2,
a1 _|_ e2,
d1
by A46, ANALMETR:83;
then A58:
a2,
a1 _|_ d2,
d1
by A47, A56, ANALMETR:84;
consider e1' being
Element of
(Af X) such that A59:
o' <> e1'
and A60:
e1' in M'
by A22, AFF_1:32;
reconsider e1 =
e1' as
Element of
X by ANALMETR:47;
consider e2 being
Element of
X such that A61:
a3,
a2 _|_ d2,
e2
and A62:
e2 <> d2
by ANALMETR:51;
reconsider e2' =
e2 as
Element of
(Af X) by ANALMETR:47;
not
o',
e1' // e2',
d2'
proof
A63:
a2' <> a4'
proof
assume
a2' = a4'
;
:: thesis: contradiction
then
a2,
a1 // b1,
b4
by A20, ANALMETR:81;
then
b1,
b4 // b2,
b1
by A3, A12, A19, ANALMETR:82;
then
b1,
b4 // b1,
b2
by ANALMETR:81;
then
LIN b1,
b4,
b2
by ANALMETR:def 11;
then
LIN b1',
b4',
b2'
by ANALMETR:55;
then
LIN b2',
b4',
b1'
by AFF_1:15;
hence
contradiction
by A9, A10, A17, A21, A26, AFF_1:39;
:: thesis: verum
end;
assume
o',
e1' // e2',
d2'
;
:: thesis: contradiction
then
o,
e1 // e2,
d2
by ANALMETR:48;
then
o,
e1 // d2,
e2
by ANALMETR:81;
then A64:
a3,
a2 _|_ o,
e1
by A61, A62, ANALMETR:84;
o,
e1 _|_ a2,
a4
by A2, A7, A8, A23, A60, ANALMETR:78;
then
a3,
a2 // a2,
a4
by A59, A64, ANALMETR:85;
then
a2,
a4 // a2,
a3
by ANALMETR:81;
then
LIN a2,
a4,
a3
by ANALMETR:def 11;
then
LIN a2',
a4',
a3'
by ANALMETR:55;
hence
contradiction
by A7, A8, A16, A21, A63, AFF_1:39;
:: thesis: verum
end; then consider d3' being
Element of
(Af X) such that A65:
LIN o',
e1',
d3'
and A66:
LIN e2',
d2',
d3'
by AFF_1:74;
reconsider d3 =
d3' as
Element of
X by ANALMETR:47;
A67:
d3 in M
by A22, A23, A59, A60, A65, AFF_1:39;
then A68:
d3 <> d4
by A2, A22, A21, A23, A24, A30, A31, AFF_1:30;
a2,
a1 _|_ d2,
d1
by A47, A56, A57, ANALMETR:84;
then A69:
b2,
b1 _|_ d2,
d1
by A3, A12, A19, ANALMETR:84;
LIN d2',
d3',
e2'
by A66, AFF_1:15;
then
LIN d2,
d3,
e2
by ANALMETR:55;
then
d2,
d3 // d2,
e2
by ANALMETR:def 11;
then
d3,
d2 // d2,
e2
by ANALMETR:81;
then A70:
a3,
a2 _|_ d3,
d2
by A61, A62, ANALMETR:84;
then
b3,
b2 _|_ d3,
d2
by A4, A12, A18, ANALMETR:84;
then A71:
b3,
b4 _|_ d3,
d4
by A1, A2, A5, A6, A9, A10, A13, A14, A30, A43, A55, A67, A45, A69, Def3;
a1,
a4 _|_ d1,
d4
by A32, A33, A44, ANALMETR:84;
then
a3,
a4 _|_ d3,
d4
by A1, A2, A3, A4, A7, A8, A11, A12, A30, A43, A55, A58, A70, A67, Def3;
hence
a3,
a4 // b3,
b4
by A68, A71, ANALMETR:85;
:: thesis: verum end; now A72:
not
LIN o',
a2',
a1'
proof
assume
LIN o',
a2',
a1'
;
:: thesis: contradiction
then
o',
a2' // o',
a1'
by AFF_1:def 1;
hence
contradiction
by A7, A12, A15, A21, A23, A24, AFF_1:62;
:: thesis: verum
end; A73:
LIN o',
a1',
a3'
by A3, A4, A22, A23, AFF_1:33;
assume A74:
b1 = b3
;
:: thesis: a3,a4 // b3,b4then
a2,
a3 // b2,
b1
by A18, ANALMETR:81;
then A75:
a2',
a3' // b2',
b1'
by ANALMETR:48;
a2',
a1' // b2',
b1'
by A19, ANALMETR:48;
then
a2',
a1' // a2',
a3'
by A5, A13, A75, AFF_1:14;
hence
a3,
a4 // b3,
b4
by A20, A74, A72, A73, AFF_1:23;
:: thesis: verum end; hence
a3,
a4 // b3,
b4
by A27;
:: thesis: verum end;
now A76:
not
LIN o',
a1',
a4'
assume A77:
b2 = b4
;
:: thesis: a3,a4 // b3,b4
b1,
b2 // a1,
a2
by A19, ANALMETR:81;
then
a1,
a4 // a1,
a2
by A5, A13, A20, A77, ANALMETR:82;
then A78:
a1',
a4' // a1',
a2'
by ANALMETR:48;
LIN o',
a4',
a2'
by A7, A8, A21, A24, AFF_1:33;
hence
a3,
a4 // b3,
b4
by A18, A77, A78, A76, AFF_1:23;
:: thesis: verum end;
hence
a3,a4 // b3,b4
by A25; :: thesis: verum