let O, A, B be Point of (TOP-REAL 2); :: thesis: ( O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| implies ( O <> A & A <> B & O <> B & A <> O & B <> A & B <> O ) )
assume that
A1: O = |[0,0]| and
A2: A = |[0,1]| and
A3: B = |[((sqrt 3) / 2),(1 / 2)]| ; :: thesis: ( O <> A & A <> B & O <> B & A <> O & B <> A & B <> O )
( O <> A & A <> B & O <> B )

proof

( O `2 = 0 & B `2 = 1 / 2 ) by A1, A3, EUCLID:52;
hence ( O <> A & A <> B & O <> B ) by A2, EUCLID:52; :: thesis: verum

end;

hence ( O <> A & A <> B & O <> B & A <> O & B <> A & B <> O ) ; :: thesis: verum