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 ) )

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

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 A2:
F \/ {A} on L
; :: thesis: ( F on L & A on L )
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;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

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