for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 & L1 meets L2 holds
ex P being Element of plane_of_REAL n st
( P is being_plane & L1 c= P & L2 c= P )