let AS be AffinSpace; 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; 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; ( q in Plane (K,P) iff ex b being Element of AS st
( q,b // K & b in P ) )
hence
( q in Plane (K,P) iff ex b being Element of AS st
( q,b // K & b in P ) )
; verum