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