let MS be OrtAfPl; :: thesis: for a, b being Element of MS
for A, K being Subset of the carrier of MS st a <> b & ( a,b _|_ K or b,a _|_ K ) & a,b _|_ A holds
K // A
let a, b be Element of MS; :: thesis: for A, K being Subset of the carrier of MS st a <> b & ( a,b _|_ K or b,a _|_ K ) & a,b _|_ A holds
K // A
let A, K be Subset of MS; :: thesis: ( a <> b & ( a,b _|_ K or b,a _|_ K ) & a,b _|_ A implies K // A )
assume that
A1: a <> b and
A2: ( a,b _|_ K or b,a _|_ K ) and
A3: a,b _|_ A ; :: thesis: K // A
a,b _|_ K by A2, ANALMETR:49;
then consider p, q being Element of MS such that
A4: ( p <> q & K = Line (p,q) ) and
A5: a,b _|_ p,q by ANALMETR:def 13;
consider r, s being Element of MS such that
A6: ( r <> s & A = Line (r,s) ) and
A7: a,b _|_ r,s by A3, ANALMETR:def 13;
p,q // r,s by A1, A5, A7, ANALMETR:63;
hence K // A by A4, A6, ANALMETR:def 15; :: thesis: verum