let AFP be AffinPlane; :: thesis: for a, b, y being Element of AFP st a <> b holds
ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )
let a, b, y be Element of AFP; :: thesis: ( a <> b implies ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) ) )
assume A1:
a <> b
; :: thesis: ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )
A2:
now assume
not
LIN a,
b,
y
;
:: thesis: ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )then A3:
not
LIN b,
a,
y
by AFF_1:15;
consider x being
Element of
AFP such that A4:
(
b,
a // y,
x &
b,
y // a,
x )
by DIRAF:47;
A5:
not
LIN a,
b,
x
by A3, A4, Lm5;
(
a,
b // x,
y &
a,
x // b,
y )
by A4, AFF_1:13;
hence
ex
x being
Element of
AFP st
( ( not
LIN a,
b,
x &
a,
b // x,
y &
a,
x // b,
y ) or (
LIN a,
b,
x & ex
p,
q being
Element of
AFP st
( not
LIN a,
b,
p &
a,
b // p,
q &
a,
p // b,
q &
p,
q // x,
y &
p,
x // q,
y ) ) )
by A5;
:: thesis: verum end;
now assume A6:
LIN a,
b,
y
;
:: thesis: ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )consider p being
Element of
AFP such that A7:
not
LIN a,
b,
p
by A1, AFF_1:22;
consider q being
Element of
AFP such that A8:
(
a,
b // p,
q &
a,
p // b,
q )
by DIRAF:47;
consider x being
Element of
AFP such that A9:
(
q,
p // y,
x &
q,
y // p,
x )
by DIRAF:47;
A10:
(
p,
q // x,
y &
p,
x // q,
y )
by A9, AFF_1:13;
LIN a,
b,
x
proof
A11:
(
a,
b // x,
y or
p = q )
by A8, A10, AFF_1:14;
then
a,
b // y,
x
by A11, AFF_1:13;
hence
LIN a,
b,
x
by A1, A6, AFF_1:18;
:: thesis: verum
end; hence
ex
x being
Element of
AFP st
( ( not
LIN a,
b,
x &
a,
b // x,
y &
a,
x // b,
y ) or (
LIN a,
b,
x & ex
p,
q being
Element of
AFP st
( not
LIN a,
b,
p &
a,
b // p,
q &
a,
p // b,
q &
p,
q // x,
y &
p,
x // q,
y ) ) )
by A7, A8, A10;
:: thesis: verum end;
hence
ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )
by A2; :: thesis: verum