let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: for X being non empty lower Subset of L holds Bottom L in X

let X be non empty lower Subset of L; :: thesis: Bottom L in X

consider y being object such that

A1: y in X by XBOOLE_0:def 1;

reconsider y = y as Element of X by A1;

Bottom L <= y by YELLOW_0:44;

hence Bottom L in X by WAYBEL_0:def 19; :: thesis: verum

let X be non empty lower Subset of L; :: thesis: Bottom L in X

consider y being object such that

A1: y in X by XBOOLE_0:def 1;

reconsider y = y as Element of X by A1;

Bottom L <= y by YELLOW_0:44;

hence Bottom L in X by WAYBEL_0:def 19; :: thesis: verum