let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in y=0-line or x in y>=0-plane )
assume x in y=0-line ; :: thesis: x in y>=0-plane
then reconsider x = x as Element of y=0-line ;
A1: x = |[(x `1),(x `2)]| by EUCLID:53;
then x `2 = 0 by Th15;
hence x in y>=0-plane by A1; :: thesis: verum