let X, x be set ; :: thesis: for R being Subset-Family of X st x in X holds
( x in Intersect R iff for Y being set st Y in R holds
x in Y )
let R be Subset-Family of X; :: thesis: ( x in X implies ( x in Intersect R iff for Y being set st Y in R holds
x in Y ) )
assume A1: x in X ; :: thesis: ( x in Intersect R iff for Y being set st Y in R holds
x in Y )

hereby :: thesis: ( ( for Y being set st Y in R holds
x in Y ) implies x in Intersect R )

assume A2: x in Intersect R ; :: thesis: for Y being set st Y in R holds
x in Y
let Y be set ; :: thesis: ( Y in R implies x in Y )
assume A3: Y in R ; :: thesis: x in Y
then Intersect R = meet R by Def9;
hence x in Y by A2, A3, Def1; :: thesis: verum

end;

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

per cases ( R <> {} or R = {} ) ;

suppose A5: R <> {} ; :: thesis: x in Intersect R

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

end;

suppose R = {} ; :: thesis: x in Intersect R

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

end;

end;