let S be IncStruct ; 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; for P being PLANE of S holds
( {A,B} on P iff ( A on P & B on P ) )
let P be PLANE of S; ( {A,B} on P iff ( A on P & B on P ) )
thus
( {A,B} on P implies ( A on P & B on P ) )
( A on P & B on P implies {A,B} on P )
assume A2:
( A on P & B on P )
; {A,B} on P
let C be POINT of S; INCSP_1:def 5 ( C in {A,B} implies C on P )
assume
C in {A,B}
; C on P
hence
C on P
by A2, TARSKI:def 2; verum