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

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

end;assume A3: x in Z ; :: thesis: x in meet X

for Y being set st Y in X holds

x in Y

proof

hence
x in meet X
by A1, Def1; :: thesis: verum
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;assume Y in X ; :: thesis: x in Y

then Z c= Y by A2;

hence x in Y by A3; :: thesis: verum