let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, a1, b1, c1 being Element of S st b out a,c & b1 out a1,c1 & b,a equiv b1,a1 & b,c equiv b1,c1 holds
a,c equiv a1,c1
let a, b, c, a1, b1, c1 be Element of S; :: thesis: ( b out a,c & b1 out a1,c1 & b,a equiv b1,a1 & b,c equiv b1,c1 implies a,c equiv a1,c1 )
assume that
A1: b out a,c and
A2: b1 out a1,c1 and
A3: b,a equiv b1,a1 and
A4: b,c equiv b1,c1 and
A5: not a,c equiv a1,c1 ; :: thesis: contradiction
now :: thesis: ( b out c,a & b1 out c1,a1 & not c,a equiv c1,a1 & a,b equiv a1,b1 & c,b equiv c1,b1 & ( not between c,a,b or not between c1,a1,b1 ) & ( not between a,c,b or not between a1,c1,b1 ) & ( b,a <= b,c or b1,c1 <= b1,a1 ) & ( b,c <= b,a or b1,a1 <= b1,c1 ) )
thus b out c,a by A1; :: thesis: ( b1 out c1,a1 & not c,a equiv c1,a1 & a,b equiv a1,b1 & c,b equiv c1,b1 & ( not between c,a,b or not between c1,a1,b1 ) & ( not between a,c,b or not between a1,c1,b1 ) & ( b,a <= b,c or b1,c1 <= b1,a1 ) & ( b,c <= b,a or b1,a1 <= b1,c1 ) )
thus b1 out c1,a1 by A2; :: thesis: ( not c,a equiv c1,a1 & a,b equiv a1,b1 & c,b equiv c1,b1 & ( not between c,a,b or not between c1,a1,b1 ) & ( not between a,c,b or not between a1,c1,b1 ) & ( b,a <= b,c or b1,c1 <= b1,a1 ) & ( b,c <= b,a or b1,a1 <= b1,c1 ) )
( b,a equiv a1,b1 & b,c equiv c1,b1 & not a,c equiv c1,a1 ) by Satz2p5, A3, A4, A5;
hence ( not c,a equiv c1,a1 & a,b equiv a1,b1 & c,b equiv c1,b1 ) by Satz2p4; :: thesis: ( ( not between c,a,b or not between c1,a1,b1 ) & ( not between a,c,b or not between a1,c1,b1 ) & ( b,a <= b,c or b1,c1 <= b1,a1 ) & ( b,c <= b,a or b1,a1 <= b1,c1 ) )
hence ( ( not between c,a,b or not between c1,a1,b1 ) & ( not between a,c,b or not between a1,c1,b1 ) ) by Satz4p3, A5; :: thesis: ( ( b,a <= b,c or b1,c1 <= b1,a1 ) & ( b,c <= b,a or b1,a1 <= b1,c1 ) )
thus ( ( b,a <= b,c or b1,c1 <= b1,a1 ) & ( b,c <= b,a or b1,a1 <= b1,c1 ) ) by A3, Satz6p28Lem02, A4; :: thesis: verum
end;
hence contradiction by Satz6p28Lem01, A1, A2, Satz3p2; :: thesis: verum