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

proof

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;

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