let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for A being Subset of S st A is_line holds
for E1, E2 being Subset of S st E1 is_plane & E2 is_plane & A c= E1 & A c= E2 & E1 <> E2 holds
for x being POINT of S holds
( ( x in E1 & x in E2 ) iff x in A )
let A be Subset of S; :: thesis: ( A is_line implies for E1, E2 being Subset of S st E1 is_plane & E2 is_plane & A c= E1 & A c= E2 & E1 <> E2 holds
for x being POINT of S holds
( ( x in E1 & x in E2 ) iff x in A ) )
assume A1: A is_line ; :: thesis: for E1, E2 being Subset of S st E1 is_plane & E2 is_plane & A c= E1 & A c= E2 & E1 <> E2 holds
for x being POINT of S holds
( ( x in E1 & x in E2 ) iff x in A )
let E1, E2 be Subset of S; :: thesis: ( E1 is_plane & E2 is_plane & A c= E1 & A c= E2 & E1 <> E2 implies for x being POINT of S holds
( ( x in E1 & x in E2 ) iff x in A ) )
assume that
A2: E1 is_plane and
A3: E2 is_plane and
A4: A c= E1 and
A5: A c= E2 and
A6: E1 <> E2 ; :: thesis: for x being POINT of S holds
( ( x in E1 & x in E2 ) iff x in A )
consider a, b being POINT of S such that
a <> b and
A7: A = Line (a,b) by A1;
let x be POINT of S; :: thesis: ( ( x in E1 & x in E2 ) iff x in A )

hereby :: thesis: ( x in A implies ( x in E1 & x in E2 ) )

assume that
A8: x in E1 and
A9: x in E2 ; :: thesis: x in A

per cases ( ( x <> a & x <> b ) or x = a or x = b ) ;

suppose ( x <> a & x <> b ) ; :: thesis: x in A

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: x in A

hence x in A ; :: thesis: verum

end;

suppose A10: not x in A ; :: thesis: x in A

( not Collinear a,b,x & a in E1 & b in E1 & a in E2 & b in E2 ) by A4, A5, A7, A10, GTARSKI3:83;
hence x in A by A2, A3, A6, A8, A9, Th52; :: thesis: verum

end;

end;

end;

suppose ( x = a or x = b ) ; :: thesis: x in A

hence x in A by A7, GTARSKI3:83; :: thesis: verum

end;

end;

end;

assume x in A ; :: thesis: ( x in E1 & x in E2 )
hence ( x in E1 & x in E2 ) by A4, A5; :: thesis: verum