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 A2:
( 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 )
; :: thesis: a3,a4 // b3,b4
then A3:
( M is being_line & N is being_line )
by ANALMETR:62;
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;
reconsider M' = M, N' = N as Subset of (Af X) by ANALMETR:57;
A4:
( M' is being_line & N' is being_line )
by A3, ANALMETR:58;
not M' // N'
then
ex o' being Element of (Af X) st
( o' in M' & o' in N' )
by A4, AFF_1:72;
then consider o being Element of X such that
A5:
( o in M & o in N )
;
reconsider o' = o as Element of (Af X) by ANALMETR:47;
A6:
now assume A7:
b2 = b4
;
:: thesis: a3,a4 // b3,b4A8:
not
LIN o',
a1',
a2'
by A2, A4, A5, AFF_1:39;
A9:
LIN o',
a2',
a4'
a1',
a2' // a1',
a4'
proof
a1,
a4 // b2,
b1
by A2, A7, ANALMETR:81;
then
a2,
a1 // a1,
a4
by A2, ANALMETR:82;
then
a1,
a2 // a1,
a4
by ANALMETR:81;
hence
a1',
a2' // a1',
a4'
by ANALMETR:48;
:: thesis: verum
end; hence
a3,
a4 // b3,
b4
by A2, A7, A8, A9, AFF_1:23;
:: thesis: verum end;
now assume A10:
b2 <> b4
;
:: thesis: a3,a4 // b3,b4A11:
now assume A12:
b1 = b3
;
:: thesis: a3,a4 // b3,b4A13:
not
LIN o',
a2',
a1'
by A2, A4, A5, AFF_1:39;
A14:
LIN o',
a1',
a3'
a2',
a1' // a2',
a3'
proof
a2,
a1 // b3,
b2
by A2, A12, ANALMETR:81;
then
a2,
a1 // a3,
a2
by A2, ANALMETR:82;
then
a2,
a1 // a2,
a3
by ANALMETR:81;
hence
a2',
a1' // a2',
a3'
by ANALMETR:48;
:: thesis: verum
end; hence
a3,
a4 // b3,
b4
by A2, A12, A13, A14, AFF_1:23;
:: thesis: verum end; now assume A15:
b1 <> b3
;
:: thesis: a3,a4 // b3,b4A16:
(
a1 <> a3 &
a2 <> a4 )
proof
assume
(
a1 = a3 or
a2 = a4 )
;
:: thesis: contradiction
then
(
a2,
a1 // b3,
b2 or
a1,
a4 // b2,
b1 )
by A2, ANALMETR:81;
then
(
b3,
b2 // b2,
b1 or
b2,
b1 // b1,
b4 )
by A2, 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 A2, A4, A10, A15, AFF_1:39;
:: thesis: verum
end; consider d3' being
Element of
(Af X) such that A17:
(
o' <> d3' &
d3' in N' )
by A4, AFF_1:32;
consider d3 being
Element of
X such that A18:
(
d3 in N &
d3 <> o )
by A17;
reconsider d3' =
d3 as
Element of
(Af X) by ANALMETR:47;
consider e1 being
Element of
X such that A19:
(
a3,
a1 // a3,
e1 &
a3 <> e1 )
by ANALMETR:51;
consider e2 being
Element of
X such that A20:
(
a3,
a2 _|_ d3,
e2 &
d3 <> e2 )
by ANALMETR:def 10;
reconsider e1' =
e1,
e2' =
e2 as
Element of
(Af X) by ANALMETR:47;
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 A19, ANALMETR:82;
then A21:
a3,
a2 _|_ a3,
a1
by A20, ANALMETR:84;
a3,
a1 _|_ a2,
a4
by A2, ANALMETR:78;
then
a3,
a2 // a2,
a4
by A16, A21, 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 A2, A4, A16, AFF_1:39;
:: thesis: verum
end; then consider d2' being
Element of
(Af X) such that A22:
(
LIN a3',
e1',
d2' &
LIN d3',
e2',
d2' )
by AFF_1:74;
reconsider d2 =
d2' as
Element of
X by ANALMETR:47;
A23:
d2 in M
proof
LIN a3,
e1,
d2
by A22, ANALMETR:55;
then
a3,
e1 // a3,
d2
by ANALMETR:def 11;
then
a3,
a1 // a3,
d2
by A19, ANALMETR:82;
then
LIN a3,
a1,
d2
by ANALMETR:def 11;
then
LIN a3',
a1',
d2'
by ANALMETR:55;
hence
d2 in M
by A2, A4, A16, AFF_1:39;
:: thesis: verum
end;
a3,
a2 _|_ d3,
d2
then consider d2 being
Element of
X such that A24:
(
d2 in M &
a3,
a2 _|_ d3,
d2 )
by A23;
reconsider d2' =
d2 as
Element of
(Af X) by ANALMETR:47;
consider e1 being
Element of
X such that A25:
(
a2,
a4 // a2,
e1 &
a2 <> e1 )
by ANALMETR:51;
consider e2 being
Element of
X such that A26:
(
a2,
a1 _|_ d2,
e2 &
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 A25, ANALMETR:82;
then A27:
a2,
a4 _|_ a2,
a1
by A26, ANALMETR:84;
a1,
a3 _|_ a2,
a4
by A2, ANALMETR:78;
then
a1,
a3 // a2,
a1
by A16, A27, 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 A2, A4, A16, AFF_1:39;
:: thesis: verum
end; then consider d1' being
Element of
(Af X) such that A28:
(
LIN a2',
e1',
d1' &
LIN d2',
e2',
d1' )
by AFF_1:74;
reconsider d1 =
d1' as
Element of
X by ANALMETR:47;
A29:
d1 in N
proof
LIN a2,
e1,
d1
by A28, ANALMETR:55;
then
a2,
e1 // a2,
d1
by ANALMETR:def 11;
then
a2,
a4 // a2,
d1
by A25, ANALMETR:82;
then
LIN a2,
a4,
d1
by ANALMETR:def 11;
then
LIN a2',
a4',
d1'
by ANALMETR:55;
hence
d1 in N
by A2, A4, A16, AFF_1:39;
:: thesis: verum
end; A30:
a2,
a1 _|_ d2,
d1
consider e1 being
Element of
X such that A31:
(
a1,
a3 // a1,
e1 &
a1 <> e1 )
by ANALMETR:51;
consider e2 being
Element of
X such that A32:
(
a1,
a4 _|_ d1,
e2 &
d1 <> e2 )
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 A31, ANALMETR:82;
then A33:
a1,
a3 _|_ a1,
a4
by A32, ANALMETR:84;
a1,
a3 _|_ a2,
a4
by A2, ANALMETR:78;
then
a2,
a4 // a1,
a4
by A16, A33, 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 A2, A4, A16, AFF_1:39;
:: thesis: verum
end; then consider d4' being
Element of
(Af X) such that A34:
(
LIN a1',
e1',
d4' &
LIN d1',
e2',
d4' )
by AFF_1:74;
reconsider d4 =
d4' as
Element of
X by ANALMETR:47;
A35:
d4 in M
proof
LIN a1,
e1,
d4
by A34, ANALMETR:55;
then
a1,
e1 // a1,
d4
by ANALMETR:def 11;
then
a1,
a3 // a1,
d4
by A31, ANALMETR:82;
then
LIN a1,
a3,
d4
by ANALMETR:def 11;
then
LIN a1',
a3',
d4'
by ANALMETR:55;
hence
d4 in M
by A2, A4, A16, AFF_1:39;
:: thesis: verum
end; A36:
a1,
a4 _|_ d1,
d4
then A37:
a3,
a4 _|_ d3,
d4
by A1, A2, A18, A24, A29, A30, A35, Def4;
A38:
b3,
b2 _|_ d3,
d2
by A2, A24, ANALMETR:84;
A39:
b2,
b1 _|_ d2,
d1
by A2, A30, ANALMETR:84;
b1,
b4 _|_ d1,
d4
by A2, A36, ANALMETR:84;
then A40:
b3,
b4 _|_ d3,
d4
by A1, A2, A18, A24, A29, A35, A38, A39, Def4;
d3 <> d4
by A2, A4, A5, A18, A35, AFF_1:30;
hence
a3,
a4 // b3,
b4
by A37, A40, ANALMETR:85;
:: thesis: verum end; hence
a3,
a4 // b3,
b4
by A11;
:: thesis: verum end;
hence
a3,a4 // b3,b4
by A6; :: thesis: verum