let SAS be Semi_Affine_Space; :: thesis: ex x, y, z being Element of SAS st
( x <> y & y <> z & z <> x )
consider x, y, z being Element of SAS such that
A1: not x,y // x,z by Def1;
take x ; :: thesis: ex y, z being Element of SAS st
( x <> y & y <> z & z <> x )
take y ; :: thesis: ex z being Element of SAS st
( x <> y & y <> z & z <> x )
take z ; :: thesis: ( x <> y & y <> z & z <> x )
thus ( x <> y & y <> z & z <> x ) by A1, Def1, Th1, Th3; :: thesis: verum