let S be OAffinSpace; :: thesis: for x, y, z, t being Element of S st x,y '||' z,t holds
( x,y '||' t,z & y,x '||' z,t & y,x '||' t,z & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x )
let x, y, z, t be Element of S; :: thesis: ( x,y '||' z,t implies ( x,y '||' t,z & y,x '||' z,t & y,x '||' t,z & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x ) )
assume x,y '||' z,t ; :: thesis: ( x,y '||' t,z & y,x '||' z,t & y,x '||' t,z & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x )
then A1: ( x,y // z,t or x,y // t,z ) by Def4;
hence x,y '||' t,z by Def4; :: thesis: ( y,x '||' z,t & y,x '||' t,z & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x )
( y,x // t,z or y,x // z,t ) by A1, ANALOAF:def 5;
hence ( y,x '||' z,t & y,x '||' t,z ) by Def4; :: thesis: ( z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x )
( z,t // x,y or z,t // y,x ) by A1, Th5;
hence ( z,t '||' x,y & z,t '||' y,x ) by Def4; :: thesis: ( t,z '||' x,y & t,z '||' y,x )
( t,z // y,x or t,z // x,y ) by A1, Th5;
hence ( t,z '||' x,y & t,z '||' y,x ) by Def4; :: thesis: verum