let L be LATTICE; :: thesis: for a being Element of L holds
( a meets a iff a <> Bottom L )
let a be Element of L; :: thesis: ( a meets a iff a <> Bottom L )
thus ( a meets a implies a <> Bottom L ) :: thesis: ( a <> Bottom L implies a meets a )

proof

assume a meets a ; :: thesis: a <> Bottom L
then a "/\" a <> Bottom L by Def3;
hence a <> Bottom L by Th2; :: thesis: verum

end;

thus ( a <> Bottom L implies a meets a ) :: thesis: verum

proof

assume a <> Bottom L ; :: thesis: a meets a
then a "/\" a <> Bottom L by Th2;
hence a meets a by Def3; :: thesis: verum

end;