let S be OAffinSpace; :: thesis: for AS being non empty AffinStruct st AS = Lambda S holds
for a, b, c, d being Element of S
for a9, b9, c9, d9 being Element of AS st a = a9 & b = b9 & c = c9 & d = d9 holds
( a9,b9 // c9,d9 iff a,b '||' c,d )
let AS be non empty AffinStruct ; :: thesis: ( AS = Lambda S implies for a, b, c, d being Element of S
for a9, b9, c9, d9 being Element of AS st a = a9 & b = b9 & c = c9 & d = d9 holds
( a9,b9 // c9,d9 iff a,b '||' c,d ) )
assume A1: AS = Lambda S ; :: thesis: for a, b, c, d being Element of S
for a9, b9, c9, d9 being Element of AS st a = a9 & b = b9 & c = c9 & d = d9 holds
( a9,b9 // c9,d9 iff a,b '||' c,d )
let a, b, c, d be Element of S; :: thesis: for a9, b9, c9, d9 being Element of AS st a = a9 & b = b9 & c = c9 & d = d9 holds
( a9,b9 // c9,d9 iff a,b '||' c,d )
let a9, b9, c9, d9 be Element of AS; :: thesis: ( a = a9 & b = b9 & c = c9 & d = d9 implies ( a9,b9 // c9,d9 iff a,b '||' c,d ) )
assume A2: ( a = a9 & b = b9 & c = c9 & d = d9 ) ; :: thesis: ( a9,b9 // c9,d9 iff a,b '||' c,d )
thus ( a9,b9 // c9,d9 implies a,b '||' c,d ) :: thesis: ( a,b '||' c,d implies a9,b9 // c9,d9 )

proof

assume A3: [[a9,b9],[c9,d9]] in the CONGR of AS ; :: according to ANALOAF:def 2 :: thesis: a,b '||' c,d
assume not [[a,b],[c,d]] in the CONGR of S ; :: according to ANALOAF:def 2,DIRAF:def 4 :: thesis: a,b // d,c
hence [[a,b],[d,c]] in the CONGR of S by A1, A2, A3, Def1; :: according to ANALOAF:def 2 :: thesis: verum

end;

assume a,b '||' c,d ; :: thesis: a9,b9 // c9,d9
then ( a,b // c,d or a,b // d,c ) ;
then ( [[a,b],[c,d]] in the CONGR of S or [[a,b],[d,c]] in the CONGR of S ) ;
hence [[a9,b9],[c9,d9]] in the CONGR of AS by A1, A2, Def1; :: according to ANALOAF:def 2 :: thesis: verum