let Z, X be set ; :: thesis: ( Z in X implies meet X c= Z )
assume A1: Z in X ; :: thesis: meet X c= Z
meet X c= Z

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet X or x in Z )
assume x in meet X ; :: thesis: x in Z
hence x in Z by A1, Def1; :: thesis: verum

end;

hence meet X c= Z ; :: thesis: verum