let X, Y be set ; :: thesis: ( X <> {} & X c= Y implies meet Y c= meet X )
assume A1: ( X <> {} & X c= Y ) ; :: thesis: meet Y c= meet X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet Y or x in meet X )
assume x in meet Y ; :: thesis: x in meet X
then for Z being set st Z in X holds
x in Z by A1, Def1;
hence x in meet X by A1, Def1; :: thesis: verum