let X be OrtAfPl; :: thesis: ( Af X is satisfying_Scherungssatz iff X is satisfying_SCH )
A1:
( Af X is satisfying_Scherungssatz implies X is satisfying_SCH )
proof
assume A2:
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 A3:
(
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' )
;
:: thesis: a3',a4' // b3',b4'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;
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;
(
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 )
by A3, ANALMETR:48;
then
a3,
a4 // b3,
b4
by A2, A3, A4, Def3;
hence
a3',
a4' // b3',
b4'
by ANALMETR:48;
:: thesis: verum end;
hence
X is
satisfying_SCH
by CONMETR:def 6;
:: thesis: verum
end;
( X is satisfying_SCH implies Af X is satisfying_Scherungssatz )
proof
assume A5:
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 A6:
(
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 )
;
:: thesis: a3,a4 // b3,b4reconsider M' =
M,
N' =
N as
Subset of
X by ANALMETR:57;
A7:
(
M' is
being_line &
N' is
being_line )
by A6, ANALMETR:58;
reconsider a1' =
a1,
a2' =
a2,
a3' =
a3,
a4' =
a4,
b1' =
b1,
b2' =
b2,
b3' =
b3,
b4' =
b4 as
Element of
X by ANALMETR:47;
(
a3',
a2' // b3',
b2' &
a2',
a1' // b2',
b1' &
a1',
a4' // b1',
b4' )
by A6, ANALMETR:48;
then
a3',
a4' // b3',
b4'
by A5, A6, A7, 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;
hence
( Af X is satisfying_Scherungssatz iff X is satisfying_SCH )
by A1; :: thesis: verum