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 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:
a1',
a4' // a1',
a2'
A9:
LIN o',
a4',
a2'
by A2, A4, A5, AFF_1:33;
not
LIN o',
a1',
a4'
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'
A14:
LIN o',
a1',
a3'
by A2, A4, A5, AFF_1:33;
a2',
a1' // a2',
a3'
proof
A15:
a2',
a1' // b2',
b1'
by A2, ANALMETR:48;
a2,
a3 // b2,
b1
by A2, A12, ANALMETR:81;
then
a2',
a3' // b2',
b1'
by ANALMETR:48;
hence
a2',
a1' // a2',
a3'
by A2, A15, AFF_1:14;
:: thesis: verum
end; hence
a3,
a4 // b3,
b4
by A2, A12, A13, A14, AFF_1:23;
:: thesis: verum end; now assume A16:
b1 <> b3
;
:: thesis: a3,a4 // b3,b4
ex
d4' being
Element of
(Af X) st
(
o' <> d4' &
d4' in N' )
by A4, AFF_1:32;
then consider d4 being
Element of
X such that A17:
(
d4 in N &
d4 <> o )
;
reconsider d4' =
d4 as
Element of
(Af X) by ANALMETR:47;
consider e1' being
Element of
(Af X) such that A18:
(
o' <> e1' &
e1' in M' )
by A4, AFF_1:32;
reconsider e1 =
e1' as
Element of
X by ANALMETR:47;
consider e2 being
Element of
X such that A19:
(
a1,
a4 _|_ d4,
e2 &
e2 <> d4 )
by ANALMETR:51;
reconsider e2' =
e2 as
Element of
(Af X) by ANALMETR:47;
not
o',
e1' // d4',
e2'
proof
assume
o',
e1' // d4',
e2'
;
:: thesis: contradiction
then
o,
e1 // d4,
e2
by ANALMETR:48;
then A20:
o,
e1 _|_ a1,
a4
by A19, ANALMETR:84;
M' // M'
by A4, AFF_1:55;
then
o',
e1' // a1',
a3'
by A2, A5, A18, AFF_1:53;
then
o,
e1 // a1,
a3
by ANALMETR:48;
then A21:
a1,
a3 _|_ a1,
a4
by A18, A20, ANALMETR:84;
A22:
a1 <> a3
proof
assume
a1 = a3
;
:: thesis: contradiction
then
a3,
a2 // b2,
b1
by A2, ANALMETR:81;
then
b3,
b2 // b2,
b1
by A2, 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 A2, A4, A16, AFF_1:39;
:: thesis: verum
end;
A23:
a4' <> a2'
proof
assume
a4' = a2'
;
:: thesis: contradiction
then
a2,
a1 // b1,
b4
by A2, ANALMETR:81;
then
b1,
b4 // b2,
b1
by A2, 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 A2, A4, A10, AFF_1:39;
:: thesis: verum
end;
a1,
a3 _|_ a2,
a4
by A2, ANALMETR:78;
then
a1,
a4 // a2,
a4
by A21, A22, 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, A23, AFF_1:39;
:: thesis: verum
end; then consider d1' being
Element of
(Af X) such that A24:
(
LIN o',
e1',
d1' &
LIN d4',
e2',
d1' )
by AFF_1:74;
reconsider d1 =
d1' as
Element of
X by ANALMETR:47;
A25:
a1,
a4 _|_ d1,
d4
proof
LIN d4,
e2,
d1
by A24, ANALMETR:55;
then
d4,
e2 // d4,
d1
by ANALMETR:def 11;
then
d1,
d4 // d4,
e2
by ANALMETR:81;
hence
a1,
a4 _|_ d1,
d4
by A19, ANALMETR:84;
:: thesis: verum
end; then A26:
(
d1 in M &
a1,
a4 _|_ d1,
d4 )
by A4, A5, A18, A24, AFF_1:39;
consider e1' being
Element of
(Af X) such that A27:
(
o' <> e1' &
e1' in N' )
by A4, AFF_1:32;
reconsider e1 =
e1' as
Element of
X by ANALMETR:47;
consider e2 being
Element of
X such that A28:
(
a2,
a1 _|_ d1,
e2 &
e2 <> d1 )
by ANALMETR:51;
reconsider e2' =
e2 as
Element of
(Af X) by ANALMETR:47;
not
o',
e1' // e2',
d1'
proof
assume
o',
e1' // e2',
d1'
;
:: thesis: contradiction
then A29:
o,
e1 // e2,
d1
by ANALMETR:48;
a2,
a1 _|_ e2,
d1
by A28, ANALMETR:83;
then A30:
o,
e1 _|_ a2,
a1
by A28, A29, ANALMETR:84;
N' // N'
by A4, AFF_1:55;
then
o',
e1' // a2',
a4'
by A2, A5, A27, AFF_1:53;
then
o,
e1 // a2,
a4
by ANALMETR:48;
then A31:
a2,
a1 _|_ a2,
a4
by A27, A30, ANALMETR:84;
A32:
a2 <> a4
proof
assume
a2 = a4
;
:: thesis: contradiction
then
a2,
a1 // b1,
b4
by A2, ANALMETR:81;
then
b1,
b4 // b2,
b1
by A2, 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 A2, A4, A10, AFF_1:39;
:: thesis: verum
end;
A33:
a1' <> a3'
proof
assume
a1' = a3'
;
:: thesis: contradiction
then
a3,
a2 // b2,
b1
by A2, ANALMETR:81;
then
b3,
b2 // b2,
b1
by A2, 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 A2, A4, A16, AFF_1:39;
:: thesis: verum
end;
a3,
a1 _|_ a2,
a4
by A2, ANALMETR:78;
then
a3,
a1 // a2,
a1
by A31, A32, 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, A33, AFF_1:39;
:: thesis: verum
end; then consider d2' being
Element of
(Af X) such that A34:
(
LIN o',
e1',
d2' &
LIN e2',
d1',
d2' )
by AFF_1:74;
reconsider d2 =
d2' as
Element of
X by ANALMETR:47;
A35:
a2,
a1 _|_ d2,
d1
proof
LIN d1',
d2',
e2'
by A34, AFF_1:15;
then
LIN d1,
d2,
e2
by ANALMETR:55;
then
d1,
d2 // d1,
e2
by ANALMETR:def 11;
then A36:
d2,
d1 // e2,
d1
by ANALMETR:81;
a2,
a1 _|_ e2,
d1
by A28, ANALMETR:83;
hence
a2,
a1 _|_ d2,
d1
by A28, A36, ANALMETR:84;
:: thesis: verum
end; then A37:
(
d2 in N &
a2,
a1 _|_ d2,
d1 )
by A4, A5, A27, A34, AFF_1:39;
consider e1' being
Element of
(Af X) such that A38:
(
o' <> e1' &
e1' in M' )
by A4, AFF_1:32;
reconsider e1 =
e1' as
Element of
X by ANALMETR:47;
consider e2 being
Element of
X such that A39:
(
a3,
a2 _|_ d2,
e2 &
e2 <> d2 )
by ANALMETR:51;
reconsider e2' =
e2 as
Element of
(Af X) by ANALMETR:47;
not
o',
e1' // e2',
d2'
proof
assume
o',
e1' // e2',
d2'
;
:: thesis: contradiction
then
o,
e1 // e2,
d2
by ANALMETR:48;
then
o,
e1 // d2,
e2
by ANALMETR:81;
then A40:
a3,
a2 _|_ o,
e1
by A39, ANALMETR:84;
o,
e1 _|_ a2,
a4
by A2, A5, A38, ANALMETR:78;
then
a3,
a2 // a2,
a4
by A38, A40, ANALMETR:85;
then
a2,
a4 // a2,
a3
by ANALMETR:81;
then
LIN a2,
a4,
a3
by ANALMETR:def 11;
then A41:
LIN a2',
a4',
a3'
by ANALMETR:55;
a2' <> a4'
proof
assume
a2' = a4'
;
:: thesis: contradiction
then
a2,
a1 // b1,
b4
by A2, ANALMETR:81;
then
b1,
b4 // b2,
b1
by A2, 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 A2, A4, A10, AFF_1:39;
:: thesis: verum
end;
hence
contradiction
by A2, A4, A41, AFF_1:39;
:: thesis: verum
end; then consider d3' being
Element of
(Af X) such that A42:
(
LIN o',
e1',
d3' &
LIN e2',
d2',
d3' )
by AFF_1:74;
reconsider d3 =
d3' as
Element of
X by ANALMETR:47;
A43:
a3,
a2 _|_ d3,
d2
proof
LIN d2',
d3',
e2'
by A42, 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;
hence
a3,
a2 _|_ d3,
d2
by A39, ANALMETR:84;
:: thesis: verum
end; then A44:
(
d3 in M &
a3,
a2 _|_ d3,
d2 )
by A4, A5, A38, A42, AFF_1:39;
then A45:
a3,
a4 _|_ d3,
d4
by A1, A2, A17, A26, A37, Def3;
A46:
b1,
b4 _|_ d1,
d4
by A2, A25, ANALMETR:84;
A47:
b2,
b1 _|_ d2,
d1
by A2, A35, ANALMETR:84;
A48:
b3,
b2 _|_ d3,
d2
by A2, A43, ANALMETR:84;
A49:
d3 <> d4
by A2, A4, A5, A17, A44, AFF_1:30;
b3,
b4 _|_ d3,
d4
by A1, A2, A17, A26, A37, A44, A46, A47, A48, Def3;
hence
a3,
a4 // b3,
b4
by A45, A49, ANALMETR:85;
:: thesis: verum end; hence
a3,
a4 // b3,
b4
by A11;
:: thesis: verum end;
hence
a3,a4 // b3,b4
by A6; :: thesis: verum