set Z = { x where x is Point of X : for y being Point of X st y in M holds
y .|. x = 0 } ;

now :: thesis: for x0 being object st x0 in { x where x is Point of X : for y being Point of X st y in M holds
y .|. x = 0 } holds
x0 in the carrier of X

let x0 be object ; :: thesis: ( x0 in { x where x is Point of X : for y being Point of X st y in M holds
y .|. x = 0 } implies x0 in the carrier of X )
assume x0 in { x where x is Point of X : for y being Point of X st y in M holds
y .|. x = 0 } ; :: thesis: x0 in the carrier of X
then ex x being Point of X st
( x0 = x & ( for y being Point of X st y in M holds
y .|. x = 0 ) ) ;
hence x0 in the carrier of X ; :: thesis: verum

end;

then reconsider Z = { x where x is Point of X : for y being Point of X st y in M holds
y .|. x = 0 } as Subset of the carrier of X by TARSKI:def 3;
for y being Point of X st y in M holds
y .|. (0. X) = 0 by BHSP_1:15;
then 0. X in Z ;
then reconsider Z = Z as non empty Subset of the carrier of X ;
take Z ; :: thesis: for x being Point of X holds
( x in Z iff for y being Point of X st y in M holds
y .|. x = 0 )
thus for x being Point of X holds
( x in Z iff for y being Point of X st y in M holds
y .|. x = 0 ) :: thesis: verum

proof

let x be Point of X; :: thesis: ( x in Z iff for y being Point of X st y in M holds
y .|. x = 0 )

hereby :: thesis: ( ( for y being Point of X st y in M holds
y .|. x = 0 ) implies x in Z )

assume x in Z ; :: thesis: for y being Point of X st y in M holds
y .|. x = 0
then ex s being Point of X st
( x = s & ( for y being Point of X st y in M holds
y .|. s = 0 ) ) ;
hence for y being Point of X st y in M holds
y .|. x = 0 ; :: thesis: verum

end;

assume for y being Point of X st y in M holds
y .|. x = 0 ; :: thesis: x in Z
hence x in Z ; :: thesis: verum

end;