let X be OrtAfPl; :: thesis: for a, b, c being Element of X
for A being Subset of X 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 X; :: thesis: for A being Subset of X st A is being_line & a in A & b in A & c in A holds
LIN a,b,c
let A be Subset of X; :: 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 & b in A & c in A ) ; :: thesis: LIN a,b,c
reconsider A' = A as Subset of (Af X) by ANALMETR:57;
reconsider a' = a, b' = b, c' = c as Element of (Af X) by ANALMETR:47;
A' is being_line by A1, ANALMETR:58;
then LIN a',b',c' by A2, AFF_1:33;
hence LIN a,b,c by ANALMETR:55; :: thesis: verum