let X, x be set ; :: thesis:
let R be Subset-Family of X; :: thesis:
assume A1: x in X ; :: thesis:

hereby :: thesis:

assume A2: x in Intersect R ; :: thesis:
let Y be set ; :: thesis:
assume A3: Y in R ; :: thesis:
then Intersect R = meet R by Def9;
hence x in Y by A2, A3, Def1; :: thesis:

end;

assume A4: for Y being set st Y in R holds
x in Y ; :: thesis:

suppose A5: R <> {} ; :: thesis:

then x in meet R by A4, Def1;
hence x in Intersect R by A5, Def9; :: thesis:

end;

suppose R = {} ; :: thesis:

hence x in Intersect R by A1, Def9; :: thesis:

end;

end;