let A1, A2 be non empty Subset of X; :: thesis: ( ( for x being Point of X holds
( x in A1 iff for y being Point of X st y in M holds
y .|. x = 0 ) ) & ( for x being Point of X holds
( x in A2 iff for y being Point of X st y in M holds
y .|. x = 0 ) ) implies A1 = A2 )
assume that
A1: for x being Point of X holds
( x in A1 iff for y being Point of X st y in M holds
y .|. x = 0 ) and
A2: for x being Point of X holds
( x in A2 iff for y being Point of X st y in M holds
y .|. x = 0 ) ; :: thesis: A1 = A2
for x0 being object holds
( x0 in A1 iff x0 in A2 )

proof

let x0 be object ; :: thesis: ( x0 in A1 iff x0 in A2 )

hereby :: thesis: ( x0 in A2 implies x0 in A1 )

assume A3: x0 in A1 ; :: thesis: x0 in A2
then reconsider x = x0 as Point of X ;
for y being Point of X st y in M holds
y .|. x = 0 by A3, A1;
hence x0 in A2 by A2; :: thesis: verum

end;

assume A4: x0 in A2 ; :: thesis: x0 in A1
then reconsider x = x0 as Point of X ;
for y being Point of X st y in M holds
y .|. x = 0 by A4, A2;
hence x0 in A1 by A1; :: thesis: verum

end;

hence A1 = A2 by TARSKI:2; :: thesis: verum