let X be set ; :: thesis: for H, J being Subset-Family of X st H c= J holds

Intersect J c= Intersect H

let H, J be Subset-Family of X; :: thesis: ( H c= J implies Intersect J c= Intersect H )

assume A1: H c= J ; :: thesis: Intersect J c= Intersect H

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersect J or x in Intersect H )

assume A2: x in Intersect J ; :: thesis: x in Intersect H

then for Y being set st Y in H holds

x in Y by A1, Th43;

hence x in Intersect H by A2, Th43; :: thesis: verum

Intersect J c= Intersect H

let H, J be Subset-Family of X; :: thesis: ( H c= J implies Intersect J c= Intersect H )

assume A1: H c= J ; :: thesis: Intersect J c= Intersect H

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersect J or x in Intersect H )

assume A2: x in Intersect J ; :: thesis: x in Intersect H

then for Y being set st Y in H holds

x in Y by A1, Th43;

hence x in Intersect H by A2, Th43; :: thesis: verum