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

now

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

end;

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