let X be AffinPlane; :: thesis: ( X is satisfying_Scherungssatz iff ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) )
A1: ( X is satisfying_Scherungssatz implies ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) )

proof

A2: ( X is satisfying_Scherungssatz implies X is satisfying_minor_Scherungssatz )

proof

assume A3: X is satisfying_Scherungssatz ; :: thesis: X is satisfying_minor_Scherungssatz

now

let a1, 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 A4: ( 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 ( M is being_line & N is being_line ) by AFF_1:50;
hence a3,a4 // b3,b4 by A3, A4, Def3; :: thesis: verum

end;

hence X is satisfying_minor_Scherungssatz by Def1; :: thesis: verum

end;

( X is satisfying_Scherungssatz implies X is satisfying_major_Scherungssatz )

proof

assume X is satisfying_Scherungssatz ; :: thesis: X is satisfying_major_Scherungssatz
then 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 by Def3;
hence X is satisfying_major_Scherungssatz by Def2; :: thesis: verum

end;

hence ( X is satisfying_Scherungssatz implies ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) ) by A2; :: thesis: verum

end;

( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz implies X is satisfying_Scherungssatz )

proof

assume A5: ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) ; :: thesis: X is satisfying_Scherungssatz

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 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,b4

now

assume not M // N ; :: thesis: a3,a4 // b3,b4
then ex o being Element of X st
( o in M & o in N ) by A6, AFF_1:72;
hence a3,a4 // b3,b4 by A5, A6, Def2; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A5, A6, Def1; :: thesis: verum

end;

hence X is satisfying_Scherungssatz by Def3; :: thesis: verum

end;

hence ( X is satisfying_Scherungssatz iff ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) ) by A1; :: thesis: verum