thus ( CS is reflexive implies for p, q, r being Element of CS holds
( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) ) ; :: thesis: ( ( for p, q, r being Element of CS holds
( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) ) implies CS is reflexive )
assume A1: for p, q, r being Element of CS holds
( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) ; :: thesis: CS is reflexive
let p, q, r be Element of CS; :: according to COLLSP:def 3 :: thesis: ( ( not p = q & not p = r & not q = r ) or [p,q,r] in the Collinearity of CS )
assume A2: ( p = q or p = r or q = r ) ; :: thesis: [p,q,r] in the Collinearity of CS
per cases ( p = q or p = r or q = r ) by A2;
suppose p = q ; :: thesis: [p,q,r] in the Collinearity of CS
then p,q,r are_collinear by A1;
hence [p,q,r] in the Collinearity of CS ; :: thesis: verum
end;
suppose p = r ; :: thesis: [p,q,r] in the Collinearity of CS
then p,q,r are_collinear by A1;
hence [p,q,r] in the Collinearity of CS ; :: thesis: verum
end;
suppose q = r ; :: thesis: [p,q,r] in the Collinearity of CS
then p,q,r are_collinear by A1;
hence [p,q,r] in the Collinearity of CS ; :: thesis: verum
end;
end;