let S be IncStruct ; :: thesis: for A being POINT of S

for P being PLANE of S

for F being Subset of the Points of S holds

( ( F on P & A on P ) iff F \/ {A} on P )

let A be POINT of S; :: thesis: for P being PLANE of S

for F being Subset of the Points of S holds

( ( F on P & A on P ) iff F \/ {A} on P )

let P be PLANE of S; :: thesis: for F being Subset of the Points of S holds

( ( F on P & A on P ) iff F \/ {A} on P )

let F be Subset of the Points of S; :: thesis: ( ( F on P & A on P ) iff F \/ {A} on P )

thus ( F on P & A on P implies F \/ {A} on P ) :: thesis: ( F \/ {A} on P implies ( F on P & A on P ) )

hence F on P by Th7, XBOOLE_1:7; :: thesis: A on P

{A} c= F \/ {A} by XBOOLE_1:7;

then {A,A} c= F \/ {A} by ENUMSET1:29;

then {A,A} on P by A2;

hence A on P by Th3; :: thesis: verum

for P being PLANE of S

for F being Subset of the Points of S holds

( ( F on P & A on P ) iff F \/ {A} on P )

let A be POINT of S; :: thesis: for P being PLANE of S

for F being Subset of the Points of S holds

( ( F on P & A on P ) iff F \/ {A} on P )

let P be PLANE of S; :: thesis: for F being Subset of the Points of S holds

( ( F on P & A on P ) iff F \/ {A} on P )

let F be Subset of the Points of S; :: thesis: ( ( F on P & A on P ) iff F \/ {A} on P )

thus ( F on P & A on P implies F \/ {A} on P ) :: thesis: ( F \/ {A} on P implies ( F on P & A on P ) )

proof

assume A2:
F \/ {A} on P
; :: thesis: ( F on P & A on P )
assume A1:
( F on P & A on P )
; :: thesis: F \/ {A} on P

let C be POINT of S; :: according to INCSP_1:def 5 :: thesis: ( C in F \/ {A} implies C on P )

assume C in F \/ {A} ; :: thesis: C on P

then ( C in F or C in {A} ) by XBOOLE_0:def 3;

hence C on P by A1, TARSKI:def 1; :: thesis: verum

end;let C be POINT of S; :: according to INCSP_1:def 5 :: thesis: ( C in F \/ {A} implies C on P )

assume C in F \/ {A} ; :: thesis: C on P

then ( C in F or C in {A} ) by XBOOLE_0:def 3;

hence C on P by A1, TARSKI:def 1; :: thesis: verum

hence F on P by Th7, XBOOLE_1:7; :: thesis: A on P

{A} c= F \/ {A} by XBOOLE_1:7;

then {A,A} c= F \/ {A} by ENUMSET1:29;

then {A,A} on P by A2;

hence A on P by Th3; :: thesis: verum