let S be IncStruct ; :: thesis: for A being POINT of S
for L being LINE of S
for F being Subset of the Points of S holds
( ( F on L & A on L ) iff F \/ {A} on L )
let A be POINT of S; :: thesis: for L being LINE of S
for F being Subset of the Points of S holds
( ( F on L & A on L ) iff F \/ {A} on L )
let L be LINE of S; :: thesis: for F being Subset of the Points of S holds
( ( F on L & A on L ) iff F \/ {A} on L )
let F be Subset of the Points of S; :: thesis: ( ( F on L & A on L ) iff F \/ {A} on L )
thus ( F on L & A on L implies F \/ {A} on L ) :: thesis: ( F \/ {A} on L implies ( F on L & A on L ) )

proof

assume A1: ( F on L & A on L ) ; :: thesis: F \/ {A} on L
let C be POINT of S; :: according to INCSP_1:def 4 :: thesis: ( C in F \/ {A} implies C on L )
assume C in F \/ {A} ; :: thesis: C on L
then ( C in F or C in {A} ) by XBOOLE_0:def 3;
hence C on L by A1, TARSKI:def 1; :: thesis: verum

end;

assume A2: F \/ {A} on L ; :: thesis: ( F on L & A on L )
hence F on L by Th6, XBOOLE_1:7; :: thesis: A on L
{A} c= F \/ {A} by XBOOLE_1:7;
then {A,A} c= F \/ {A} by ENUMSET1:29;
then {A,A} on L by A2;
hence A on L by Th1; :: thesis: verum