let X be OrtAfPl; ( AffinStruct(# the U1 of X, the CONGR of X #) is satisfying_Scherungssatz iff X is satisfying_SCH )
A1:
( X is satisfying_SCH implies AffinStruct(# the U1 of X, the CONGR of X #) is satisfying_Scherungssatz )
proof
assume A2:
X is
satisfying_SCH
;
AffinStruct(# the U1 of X, the CONGR of X #) is satisfying_Scherungssatz
now for a1, a2, a3, a4, b1, b2, b3, b4 being Element of AffinStruct(# the U1 of X, the CONGR of X #)
for M, N being Subset of AffinStruct(# the U1 of X, the CONGR 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,b4let a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 be
Element of
AffinStruct(# the
U1 of
X, the
CONGR of
X #);
for M, N being Subset of AffinStruct(# the U1 of X, the CONGR 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,b4let M,
N be
Subset of
AffinStruct(# the
U1 of
X, the
CONGR of
X #);
( 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
;
a3,a4 // b3,b4reconsider a19 =
a1,
a29 =
a2,
a39 =
a3,
a49 =
a4,
b19 =
b1,
b29 =
b2,
b39 =
b3,
b49 =
b4 as
Element of
X ;
A24:
a39,
a29 // b39,
b29
by A21, ANALMETR:36;
A25:
a19,
a49 // b19,
b49
by A23, ANALMETR:36;
A26:
a29,
a19 // b29,
b19
by A22, ANALMETR:36;
reconsider M9 =
M,
N9 =
N as
Subset of
X ;
A27:
N9 is
being_line
by A4, ANALMETR:43;
M9 is
being_line
by A3, ANALMETR:43;
then
a39,
a49 // b39,
b49
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:36;
verum end;
hence
AffinStruct(# the
U1 of
X, the
CONGR of
X #) is
satisfying_Scherungssatz
;
verum
end;
( AffinStruct(# the U1 of X, the CONGR of X #) is satisfying_Scherungssatz implies X is satisfying_SCH )
proof
assume A28:
AffinStruct(# the
U1 of
X, the
CONGR of
X #) is
satisfying_Scherungssatz
;
X is satisfying_SCH
now for a19, a29, a39, a49, b19, b29, b39, b49 being Element of X
for M9, N9 being Subset of X st M9 is being_line & N9 is being_line & a19 in M9 & a39 in M9 & b19 in M9 & b39 in M9 & a29 in N9 & a49 in N9 & b29 in N9 & b49 in N9 & not a49 in M9 & not a29 in M9 & not b29 in M9 & not b49 in M9 & not a19 in N9 & not a39 in N9 & not b19 in N9 & not b39 in N9 & a39,a29 // b39,b29 & a29,a19 // b29,b19 & a19,a49 // b19,b49 holds
a39,a49 // b39,b49let a19,
a29,
a39,
a49,
b19,
b29,
b39,
b49 be
Element of
X;
for M9, N9 being Subset of X st M9 is being_line & N9 is being_line & a19 in M9 & a39 in M9 & b19 in M9 & b39 in M9 & a29 in N9 & a49 in N9 & b29 in N9 & b49 in N9 & not a49 in M9 & not a29 in M9 & not b29 in M9 & not b49 in M9 & not a19 in N9 & not a39 in N9 & not b19 in N9 & not b39 in N9 & a39,a29 // b39,b29 & a29,a19 // b29,b19 & a19,a49 // b19,b49 holds
a39,a49 // b39,b49let M9,
N9 be
Subset of
X;
( M9 is being_line & N9 is being_line & a19 in M9 & a39 in M9 & b19 in M9 & b39 in M9 & a29 in N9 & a49 in N9 & b29 in N9 & b49 in N9 & not a49 in M9 & not a29 in M9 & not b29 in M9 & not b49 in M9 & not a19 in N9 & not a39 in N9 & not b19 in N9 & not b39 in N9 & a39,a29 // b39,b29 & a29,a19 // b29,b19 & a19,a49 // b19,b49 implies a39,a49 // b39,b49 )assume that A29:
M9 is
being_line
and A30:
N9 is
being_line
and A31:
a19 in M9
and A32:
a39 in M9
and A33:
b19 in M9
and A34:
b39 in M9
and A35:
a29 in N9
and A36:
a49 in N9
and A37:
b29 in N9
and A38:
b49 in N9
and A39:
not
a49 in M9
and A40:
not
a29 in M9
and A41:
not
b29 in M9
and A42:
not
b49 in M9
and A43:
not
a19 in N9
and A44:
not
a39 in N9
and A45:
not
b19 in N9
and A46:
not
b39 in N9
and A47:
a39,
a29 // b39,
b29
and A48:
a29,
a19 // b29,
b19
and A49:
a19,
a49 // b19,
b49
;
a39,a49 // b39,b49reconsider a1 =
a19,
a2 =
a29,
a3 =
a39,
a4 =
a49,
b1 =
b19,
b2 =
b29,
b3 =
b39,
b4 =
b49 as
Element of
AffinStruct(# the
U1 of
X, the
CONGR of
X #) ;
A50:
a3,
a2 // b3,
b2
by A47, ANALMETR:36;
A51:
a1,
a4 // b1,
b4
by A49, ANALMETR:36;
A52:
a2,
a1 // b2,
b1
by A48, ANALMETR:36;
reconsider M =
M9,
N =
N9 as
Subset of
AffinStruct(# the
U1 of
X, the
CONGR of
X #) ;
A53:
N is
being_line
by A30, ANALMETR:43;
M is
being_line
by A29, ANALMETR:43;
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;
hence
a39,
a49 // b39,
b49
by ANALMETR:36;
verum end;
hence
X is
satisfying_SCH
by CONMETR:def 6;
verum
end;
hence
( AffinStruct(# the U1 of X, the CONGR of X #) is satisfying_Scherungssatz iff X is satisfying_SCH )
by A1; verum