let p1, p2, p3, p4, p be Point of (); :: thesis: ( ( ( p1 `1 = p2 `1 & p3 `1 = p4 `1 ) or ( p1 `2 = p2 `2 & p3 `2 = p4 `2 ) ) & (LSeg (p1,p2)) /\ (LSeg (p3,p4)) = {p} & not p = p1 & not p = p2 implies p = p3 )
assume that
A1: ( ( p1 `1 = p2 `1 & p3 `1 = p4 `1 ) or ( p1 `2 = p2 `2 & p3 `2 = p4 `2 ) ) and
A2: (LSeg (p1,p2)) /\ (LSeg (p3,p4)) = {p} ; :: thesis: ( p = p1 or p = p2 or p = p3 )
A3: p in (LSeg (p1,p2)) /\ (LSeg (p3,p4)) by ;
then p in LSeg (p3,p4) by XBOOLE_0:def 4;
then (LSeg (p3,p)) \/ (LSeg (p,p4)) = LSeg (p3,p4) by TOPREAL1:5;
then A4: LSeg (p3,p) c= LSeg (p3,p4) by XBOOLE_1:7;
A5: LSeg (p1,p2) meets LSeg (p3,p4) by A3;
A6: now :: thesis: ( p1 `2 = p2 `2 & p3 `2 = p4 `2 implies p2 `2 = p3 `2 )
assume ( p1 `2 = p2 `2 & p3 `2 = p4 `2 ) ; :: thesis: p2 `2 = p3 `2
then ( LSeg (p1,p2) is horizontal & LSeg (p3,p4) is horizontal ) by SPPOL_1:15;
hence p2 `2 = p3 `2 by ; :: thesis: verum
end;
A7: now :: thesis: ( p1 `1 = p2 `1 & p3 `1 = p4 `1 implies p2 `1 = p3 `1 )
assume ( p1 `1 = p2 `1 & p3 `1 = p4 `1 ) ; :: thesis: p2 `1 = p3 `1
then ( LSeg (p1,p2) is vertical & LSeg (p3,p4) is vertical ) by SPPOL_1:16;
hence p2 `1 = p3 `1 by ; :: thesis: verum
end;
A8: p3 in LSeg (p3,p4) by RLTOPSP1:68;
A9: p2 in LSeg (p1,p2) by RLTOPSP1:68;
A10: p1 in LSeg (p1,p2) by RLTOPSP1:68;
now :: thesis: ( p <> p1 & p <> p2 implies not p <> p3 )
A11: p in LSeg (p1,p2) by ;
assume that
A12: p <> p1 and
A13: p <> p2 and
A14: p <> p3 ; :: thesis: contradiction
A15: now :: thesis: not p3 in LSeg (p1,p2)
assume p3 in LSeg (p1,p2) ; :: thesis: contradiction
then p3 in (LSeg (p1,p2)) /\ (LSeg (p3,p4)) by ;
hence contradiction by A2, A14, TARSKI:def 1; :: thesis: verum
end;
now :: thesis: contradiction
per cases ( p1 in LSeg (p3,p) or p2 in LSeg (p3,p) ) by A1, A7, A6, A12, A13, A11, A15, Th28;
suppose p1 in LSeg (p3,p) ; :: thesis: contradiction
then p1 in (LSeg (p1,p2)) /\ (LSeg (p3,p4)) by ;
hence contradiction by A2, A12, TARSKI:def 1; :: thesis: verum
end;
suppose p2 in LSeg (p3,p) ; :: thesis: contradiction
then p2 in (LSeg (p1,p2)) /\ (LSeg (p3,p4)) by ;
hence contradiction by A2, A13, TARSKI:def 1; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence ( p = p1 or p = p2 or p = p3 ) ; :: thesis: verum