let X, Z be set ; :: thesis: ( X <> {} & ( for Z1 being set st Z1 in X holds
Z c= Z1 ) implies Z c= meet X )
assume that
A1: X <> {} and
A2: for Z1 being set st Z1 in X holds
Z c= Z1 ; :: thesis: Z c= meet X
thus Z c= meet X :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in meet X )
assume A3: x in Z ; :: thesis: x in meet X
for Y being set st Y in X holds
x in Y

proof

let Y be set ; :: thesis: ( Y in X implies x in Y )
assume Y in X ; :: thesis: x in Y
then Z c= Y by A2;
hence x in Y by A3; :: thesis: verum

end;

hence x in meet X by A1, Def1; :: thesis: verum

end;