let S be OAffinSpace; 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; ( 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 )
( [[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 )
;
DIRAF:def 4 [[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;
verum
end;
assume
[[a,b],[c,d]] in lambda the CONGR of S
; 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 )
; DIRAF:def 4 verum