let SAS be Semi_Affine_Space; :: thesis: for o, b, a, c, d being Element of SAS st o <> b & trap a,b,c,d,o holds
trap b,a,d,c,o
let o, b, a, c, d be Element of SAS; :: thesis: ( o <> b & trap a,b,c,d,o implies trap b,a,d,c,o )
assume that
A1: o <> b and
A2: trap a,b,c,d,o ; :: thesis: trap b,a,d,c,o
o,a,b is_collinear by A2, Def8;
then A3: o,b,a is_collinear by Th37;
a,c // b,d by A2, Def8;
then A4: b,d // a,c by Th17;
o,c,d is_collinear by A2, Def8;
then A5: o,d,c is_collinear by Th37;
not o,b,d is_collinear by A1, A2, Th123;
hence trap b,a,d,c,o by A3, A5, A4, Def8; :: thesis: verum