begin
definition
let X be
AffinPlane;
attr X is
satisfying_minor_Scherungssatz means :
Def1:
for
a1,
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;
end;
:: deftheorem Def1 defines satisfying_minor_Scherungssatz CONMETR1:def 1 :
for
X being
AffinPlane holds
(
X is
satisfying_minor_Scherungssatz iff for
a1,
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 );
definition
let X be
AffinPlane;
attr X is
satisfying_major_Scherungssatz means :
Def2:
for
o,
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
X for
M,
N being
Subset of
X st
M is
being_line &
N is
being_line &
o in M &
o in 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;
end;
:: deftheorem Def2 defines satisfying_major_Scherungssatz CONMETR1:def 2 :
for
X being
AffinPlane holds
(
X is
satisfying_major_Scherungssatz iff for
o,
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
X for
M,
N being
Subset of
X st
M is
being_line &
N is
being_line &
o in M &
o in 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 );
definition
let X be
AffinPlane;
attr X is
satisfying_Scherungssatz means :
Def3:
for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
X 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;
end;
:: deftheorem Def3 defines satisfying_Scherungssatz CONMETR1:def 3 :
for
X being
AffinPlane holds
(
X is
satisfying_Scherungssatz iff for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
X 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 );
definition
let X be
AffinPlane;
attr X is
satisfying_indirect_Scherungssatz means :
Def4:
for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
X for
M,
N being
Subset of
X st
M is
being_line &
N is
being_line &
a1 in M &
a3 in M &
b2 in M &
b4 in M &
a2 in N &
a4 in N &
b1 in N &
b3 in N & not
a4 in M & not
a2 in M & not
b1 in M & not
b3 in M & not
a1 in N & not
a3 in N & not
b2 in N & not
b4 in N &
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 holds
a3,
a4 // b3,
b4;
end;
:: deftheorem Def4 defines satisfying_indirect_Scherungssatz CONMETR1:def 4 :
for
X being
AffinPlane holds
(
X is
satisfying_indirect_Scherungssatz iff for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
X for
M,
N being
Subset of
X st
M is
being_line &
N is
being_line &
a1 in M &
a3 in M &
b2 in M &
b4 in M &
a2 in N &
a4 in N &
b1 in N &
b3 in N & not
a4 in M & not
a2 in M & not
b1 in M & not
b3 in M & not
a1 in N & not
a3 in N & not
b2 in N & not
b4 in N &
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 holds
a3,
a4 // b3,
b4 );
definition
let X be
AffinPlane;
attr X is
satisfying_minor_indirect_Scherungssatz means :
Def5:
for
a1,
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 &
b2 in M &
b4 in M &
a2 in N &
a4 in N &
b1 in N &
b3 in N & not
a4 in M & not
a2 in M & not
b1 in M & not
b3 in M & not
a1 in N & not
a3 in N & not
b2 in N & not
b4 in N &
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 holds
a3,
a4 // b3,
b4;
end;
:: deftheorem Def5 defines satisfying_minor_indirect_Scherungssatz CONMETR1:def 5 :
for
X being
AffinPlane holds
(
X is
satisfying_minor_indirect_Scherungssatz iff for
a1,
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 &
b2 in M &
b4 in M &
a2 in N &
a4 in N &
b1 in N &
b3 in N & not
a4 in M & not
a2 in M & not
b1 in M & not
b3 in M & not
a1 in N & not
a3 in N & not
b2 in N & not
b4 in N &
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 holds
a3,
a4 // b3,
b4 );
definition
let X be
AffinPlane;
attr X is
satisfying_major_indirect_Scherungssatz means :
Def6:
for
o,
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
X for
M,
N being
Subset of
X st
M is
being_line &
N is
being_line &
o in M &
o in N &
a1 in M &
a3 in M &
b2 in M &
b4 in M &
a2 in N &
a4 in N &
b1 in N &
b3 in N & not
a4 in M & not
a2 in M & not
b1 in M & not
b3 in M & not
a1 in N & not
a3 in N & not
b2 in N & not
b4 in N &
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 holds
a3,
a4 // b3,
b4;
end;
:: deftheorem Def6 defines satisfying_major_indirect_Scherungssatz CONMETR1:def 6 :
for
X being
AffinPlane holds
(
X is
satisfying_major_indirect_Scherungssatz iff for
o,
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
X for
M,
N being
Subset of
X st
M is
being_line &
N is
being_line &
o in M &
o in N &
a1 in M &
a3 in M &
b2 in M &
b4 in M &
a2 in N &
a4 in N &
b1 in N &
b3 in N & not
a4 in M & not
a2 in M & not
b1 in M & not
b3 in M & not
a1 in N & not
a3 in N & not
b2 in N & not
b4 in N &
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 holds
a3,
a4 // b3,
b4 );
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem
theorem
theorem
theorem
theorem
theorem
theorem