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 )

x in Y ; :: thesis: x in Intersect R

( 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 A4:
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;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

x in Y ; :: thesis: x in Intersect R