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 ) )

( q,b // K & b in P ) ) ; :: thesis: verum

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 ) )

hence
( q in Plane (K,P) iff 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;( 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

( q,b // K & b in P ) ) ; :: thesis: verum