let X be OrtAfPl; :: thesis: ( Af X is satisfying_Scherungssatz iff X is satisfying_SCH )
A1:
( X is satisfying_SCH implies Af X is satisfying_Scherungssatz )
proof
assume A2:
X is
satisfying_SCH
;
:: thesis: Af X is satisfying_Scherungssatz
now let a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 be
Element of
(Af X);
:: thesis: for M, N being Subset of (Af X) st M is being_line & N is being_line & 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,b4let M,
N be
Subset of
(Af X);
:: thesis: ( M is being_line & N is being_line & 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 A3:
M is
being_line
and A4:
N is
being_line
and A5:
a1 in M
and A6:
a3 in M
and A7:
b1 in M
and A8:
b3 in M
and A9:
a2 in N
and A10:
a4 in N
and A11:
b2 in N
and A12:
b4 in N
and A13:
not
a4 in M
and A14:
not
a2 in M
and A15:
not
b2 in M
and A16:
not
b4 in M
and A17:
not
a1 in N
and A18:
not
a3 in N
and A19:
not
b1 in N
and A20:
not
b3 in N
and A21:
a3,
a2 // b3,
b2
and A22:
a2,
a1 // b2,
b1
and A23:
a1,
a4 // b1,
b4
;
:: thesis: a3,a4 // b3,b4reconsider a1' =
a1,
a2' =
a2,
a3' =
a3,
a4' =
a4,
b1' =
b1,
b2' =
b2,
b3' =
b3,
b4' =
b4 as
Element of
X by ANALMETR:47;
A24:
a3',
a2' // b3',
b2'
by A21, ANALMETR:48;
A25:
a1',
a4' // b1',
b4'
by A23, ANALMETR:48;
A26:
a2',
a1' // b2',
b1'
by A22, ANALMETR:48;
reconsider M' =
M,
N' =
N as
Subset of
X by ANALMETR:57;
A27:
N' is
being_line
by A4, ANALMETR:58;
M' is
being_line
by A3, ANALMETR:58;
then
a3',
a4' // b3',
b4'
by A2, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A27, A24, A26, A25, CONMETR:def 6;
hence
a3,
a4 // b3,
b4
by ANALMETR:48;
:: thesis: verum end;
hence
Af X is
satisfying_Scherungssatz
by Def3;
:: thesis: verum
end;
( Af X is satisfying_Scherungssatz implies X is satisfying_SCH )
proof
assume A28:
Af X is
satisfying_Scherungssatz
;
:: thesis: X is satisfying_SCH
now let a1',
a2',
a3',
a4',
b1',
b2',
b3',
b4' be
Element of
X;
:: thesis: for M', N' being Subset of X st M' is being_line & N' is being_line & 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' is being_line & N' is being_line & 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 A29:
M' is
being_line
and A30:
N' is
being_line
and A31:
a1' in M'
and A32:
a3' in M'
and A33:
b1' in M'
and A34:
b3' in M'
and A35:
a2' in N'
and A36:
a4' in N'
and A37:
b2' in N'
and A38:
b4' in N'
and A39:
not
a4' in M'
and A40:
not
a2' in M'
and A41:
not
b2' in M'
and A42:
not
b4' in M'
and A43:
not
a1' in N'
and A44:
not
a3' in N'
and A45:
not
b1' in N'
and A46:
not
b3' in N'
and A47:
a3',
a2' // b3',
b2'
and A48:
a2',
a1' // b2',
b1'
and A49:
a1',
a4' // b1',
b4'
;
:: thesis: a3',a4' // b3',b4'reconsider a1 =
a1',
a2 =
a2',
a3 =
a3',
a4 =
a4',
b1 =
b1',
b2 =
b2',
b3 =
b3',
b4 =
b4' as
Element of
(Af X) by ANALMETR:47;
A50:
a3,
a2 // b3,
b2
by A47, ANALMETR:48;
A51:
a1,
a4 // b1,
b4
by A49, ANALMETR:48;
A52:
a2,
a1 // b2,
b1
by A48, ANALMETR:48;
reconsider M =
M',
N =
N' as
Subset of
(Af X) by ANALMETR:57;
A53:
N is
being_line
by A30, ANALMETR:58;
M is
being_line
by A29, ANALMETR:58;
then
a3,
a4 // b3,
b4
by A28, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A53, A50, A52, A51, Def3;
hence
a3',
a4' // b3',
b4'
by ANALMETR:48;
:: thesis: verum end;
hence
X is
satisfying_SCH
by CONMETR:def 6;
:: thesis: verum
end;
hence
( Af X is satisfying_Scherungssatz iff X is satisfying_SCH )
by A1; :: thesis: verum