let AFS be AffinSpace; :: thesis: for a, b, c, d being Element of AFS holds

( not a,b // c,d or a,c // b,d or ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) )

let a, b, c, d be Element of AFS; :: thesis: ( not a,b // c,d or a,c // b,d or ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) )

assume A1: a,b // c,d ; :: thesis: ( a,c // b,d or ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) )

assume A2: not a,c // b,d ; :: thesis: ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x )

( LIN a,c,x & LIN b,d,x ) by A3; :: thesis: verum

( not a,b // c,d or a,c // b,d or ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) )

let a, b, c, d be Element of AFS; :: thesis: ( not a,b // c,d or a,c // b,d or ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) )

assume A1: a,b // c,d ; :: thesis: ( a,c // b,d or ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) )

assume A2: not a,c // b,d ; :: thesis: ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x )

A3: now :: thesis: ( a <> b implies ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) )

( LIN a,c,x & LIN b,d,x ) )

consider z being Element of AFS such that

A4: a,b // c,z and

A5: a,c // b,z by DIRAF:40;

assume A6: a <> b ; :: thesis: ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x )

( LIN a,c,x & LIN b,d,x ) by A7; :: thesis: verum

end;A4: a,b // c,z and

A5: a,c // b,z by DIRAF:40;

assume A6: a <> b ; :: thesis: ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x )

A7: now :: thesis: ( b <> z implies ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) )

( LIN a,c,x & LIN b,d,x ) )

c,d // c,z
by A1, A6, A4, AFF_1:5;

then LIN c,d,z by AFF_1:def 1;

then LIN d,c,z by AFF_1:6;

then d,c // d,z by AFF_1:def 1;

then z,d // d,c by AFF_1:4;

then consider t being Element of AFS such that

A8: b,d // d,t and

A9: b,z // c,t by A2, A5, DIRAF:40;

assume b <> z ; :: thesis: ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x )

then a,c // c,t by A5, A9, AFF_1:5;

then c,a // c,t by AFF_1:4;

then LIN c,a,t by AFF_1:def 1;

then A10: LIN a,c,t by AFF_1:6;

d,b // d,t by A8, AFF_1:4;

then LIN d,b,t by AFF_1:def 1;

then LIN b,d,t by AFF_1:6;

hence ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) by A10; :: thesis: verum

end;then LIN c,d,z by AFF_1:def 1;

then LIN d,c,z by AFF_1:6;

then d,c // d,z by AFF_1:def 1;

then z,d // d,c by AFF_1:4;

then consider t being Element of AFS such that

A8: b,d // d,t and

A9: b,z // c,t by A2, A5, DIRAF:40;

assume b <> z ; :: thesis: ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x )

then a,c // c,t by A5, A9, AFF_1:5;

then c,a // c,t by AFF_1:4;

then LIN c,a,t by AFF_1:def 1;

then A10: LIN a,c,t by AFF_1:6;

d,b // d,t by A8, AFF_1:4;

then LIN d,b,t by AFF_1:def 1;

then LIN b,d,t by AFF_1:6;

hence ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) by A10; :: thesis: verum

now :: thesis: ( b = z implies ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) )

hence
ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) )

assume
b = z
; :: thesis: ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x )

then b,a // b,c by A4, AFF_1:4;

then LIN b,a,c by AFF_1:def 1;

then A11: LIN a,c,b by AFF_1:6;

LIN b,d,b by AFF_1:7;

hence ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) by A11; :: thesis: verum

end;( LIN a,c,x & LIN b,d,x )

then b,a // b,c by A4, AFF_1:4;

then LIN b,a,c by AFF_1:def 1;

then A11: LIN a,c,b by AFF_1:6;

LIN b,d,b by AFF_1:7;

hence ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) by A11; :: thesis: verum

( LIN a,c,x & LIN b,d,x ) by A7; :: thesis: verum

now :: thesis: ( a = b implies ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) )

hence
ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) )

assume
a = b
; :: thesis: ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x )

then ( LIN a,c,a & LIN b,d,a ) by AFF_1:7;

hence ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) ; :: thesis: verum

end;( LIN a,c,x & LIN b,d,x )

then ( LIN a,c,a & LIN b,d,a ) by AFF_1:7;

hence ex x being Element of AFS st

( LIN a,c,x & LIN b,d,x ) ; :: thesis: verum

( LIN a,c,x & LIN b,d,x ) by A3; :: thesis: verum