let AS be AffinSpace; :: thesis: for X being Subset of AS st X is being_line holds
for x being set holds
( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) )
let X be Subset of AS; :: thesis: ( X is being_line implies for x being set holds
( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) ) )
assume A1: X is being_line ; :: thesis: for x being set holds
( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) )
let x be set ; :: thesis: ( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) )
A2: now :: thesis: ( x in LDir X implies ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) )
assume x in LDir X ; :: thesis: ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y )
then [x,X] in LinesParallelity AS by EQREL_1:19;
then consider K, M being Subset of AS such that
A3: [x,X] = [K,M] and
A4: K is being_line and
A5: M is being_line and
A6: K '||' M ;
take Y = K; :: thesis: ( x = Y & Y is being_line & X '||' Y )
A7: X = M by A3, XTUPLE_0:1;
K // M by A4, A5, A6, AFF_4:40;
hence ( x = Y & Y is being_line & X '||' Y ) by A3, A4, A5, A7, AFF_4:40, XTUPLE_0:1; :: thesis: verum
end;
now :: thesis: ( ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) implies x in LDir X )
given Y being Subset of AS such that A8: x = Y and
A9: Y is being_line and
A10: X '||' Y ; :: thesis: x in LDir X
X // Y by A1, A9, A10, AFF_4:40;
then Y '||' X by A1, A9, AFF_4:40;
then [Y,X] in { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } by A1, A9;
hence x in LDir X by A8, EQREL_1:19; :: thesis: verum
end;
hence ( x in LDir X iff ex Y being Subset of AS st
( x = Y & Y is being_line & X '||' Y ) ) by A2; :: thesis: verum