let X be OrtAfPl; :: thesis: for a, b, c being Element of
for A being Subset of st A is being_line & a in A & b in A & c in A holds
LIN a,b,c
let a, b, c be Element of ; :: thesis: for A being Subset of st A is being_line & a in A & b in A & c in A holds
LIN a,b,c
let A be Subset of ; :: thesis: ( A is being_line & a in A & b in A & c in A implies LIN a,b,c )
assume that
A1: A is being_line and
A2: a in A and
A3: b in A and
A4: c in A ; :: thesis: LIN a,b,c
reconsider a' = a, b' = b, c' = c as Element of by ANALMETR:47;
reconsider A' = A as Subset of by ANALMETR:57;
A' is being_line by A1, ANALMETR:58;
then LIN a',b',c' by A2, A3, A4, AFF_1:33;
hence LIN a,b,c by ANALMETR:55; :: thesis: verum