let S be OAffinSpace; :: thesis: for a, b, c, d being Element of S holds
( a,b '||' c,d iff [[a,b],[c,d]] in lambda the CONGR of S )
let a, b, c, d be Element of S; :: thesis: ( a,b '||' c,d iff [[a,b],[c,d]] in lambda the CONGR of S )
thus ( a,b '||' c,d implies [[a,b],[c,d]] in lambda the CONGR of S ) :: thesis: ( [[a,b],[c,d]] in lambda the CONGR of S implies a,b '||' c,d )

proof

assume ( a,b // c,d or a,b // d,c ) ; :: according to DIRAF:def 4 :: thesis: [[a,b],[c,d]] in lambda the CONGR of S
then ( [[a,b],[c,d]] in the CONGR of S or [[a,b],[d,c]] in the CONGR of S ) ;
hence [[a,b],[c,d]] in lambda the CONGR of S by Def1; :: thesis: verum

end;

assume [[a,b],[c,d]] in lambda the CONGR of S ; :: thesis: a,b '||' c,d
then ( [[a,b],[c,d]] in the CONGR of S or [[a,b],[d,c]] in the CONGR of S ) by Def1;
hence ( a,b // c,d or a,b // d,c ) ; :: according to DIRAF:def 4 :: thesis: verum