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