let S be IncStruct ; :: thesis: for A, B being POINT of S
for P being PLANE of S holds
( {A,B} on P iff ( A on P & B on P ) )
let A, B be POINT of S; :: thesis: for P being PLANE of S holds
( {A,B} on P iff ( A on P & B on P ) )
let P be PLANE of S; :: thesis: ( {A,B} on P iff ( A on P & B on P ) )
thus ( {A,B} on P implies ( A on P & B on P ) ) :: thesis: ( A on P & B on P implies {A,B} on P )

proof

assume A1: {A,B} on P ; :: thesis: ( A on P & B on P )
( A in {A,B} & B in {A,B} ) by TARSKI:def 2;
hence ( A on P & B on P ) by A1, Def5; :: thesis: verum

end;

assume A2: ( A on P & B on P ) ; :: thesis: {A,B} on P
let C be POINT of S; :: according to INCSP_1:def 5 :: thesis: ( C in {A,B} implies C on P )
assume C in {A,B} ; :: thesis: C on P
hence C on P by A2, TARSKI:def 2; :: thesis: verum