let AS be AffinSpace; :: thesis: for K, P being Subset of AS
for q being Element of AS holds
( q in Plane (K,P) iff ex b being Element of AS st
( q,b // K & b in P ) )
let K, P be Subset of AS; :: thesis: for q being Element of AS holds
( q in Plane (K,P) iff ex b being Element of AS st
( q,b // K & b in P ) )
let q be Element of AS; :: thesis: ( q in Plane (K,P) iff ex b being Element of AS st
( q,b // K & b in P ) )

now :: thesis: ( q in Plane (K,P) implies ex b being Element of AS st
( q,b // K & b in P ) )

assume q in Plane (K,P) ; :: thesis: ex b being Element of AS st
( q,b // K & b in P )
then ex a being Element of AS st
( a = q & ex b being Element of AS st
( a,b // K & b in P ) ) ;
hence ex b being Element of AS st
( q,b // K & b in P ) ; :: thesis: verum

end;

hence ( q in Plane (K,P) iff ex b being Element of AS st
( q,b // K & b in P ) ) ; :: thesis: verum