let AFP be AffinPlane; for a, b, x being Element of AFP st a <> b holds
ex y 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, x be Element of AFP; ( a <> b implies ex y 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
; ex y 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 ( LIN a,b,x implies ex y 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 A3:
LIN a,
b,
x
;
ex y 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 A4:
not
LIN a,
b,
p
by A1, AFF_1:13;
consider q being
Element of
AFP such that A5:
(
a,
b // p,
q &
a,
p // b,
q )
by DIRAF:40;
ex
y being
Element of
AFP st
(
p,
q // x,
y &
p,
x // q,
y )
by DIRAF:40;
hence
ex
y 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 A3, A4, A5;
verum end;
now ( not LIN a,b,x implies ex y 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 ) ) ) )A6:
ex
y being
Element of
AFP st
(
a,
b // x,
y &
a,
x // b,
y )
by DIRAF:40;
assume
not
LIN a,
b,
x
;
ex y 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 ) ) )hence
ex
y 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 A6;
verum end;
hence
ex y 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; verum