let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: for S being with_bottom Subset of L holds subrelstr S is lower-bounded

let S be with_bottom Subset of L; :: thesis: subrelstr S is lower-bounded

Bottom L in S by Def8;

then reconsider dL = Bottom L as Element of (subrelstr S) by YELLOW_0:def 15;

take dL ; :: according to YELLOW_0:def 4 :: thesis: dL is_<=_than the carrier of (subrelstr S)

let S be with_bottom Subset of L; :: thesis: subrelstr S is lower-bounded

Bottom L in S by Def8;

then reconsider dL = Bottom L as Element of (subrelstr S) by YELLOW_0:def 15;

take dL ; :: according to YELLOW_0:def 4 :: thesis: dL is_<=_than the carrier of (subrelstr S)

now :: thesis: for x being Element of (subrelstr S) st x in the carrier of (subrelstr S) holds

dL <= x

hence
dL is_<=_than the carrier of (subrelstr S)
; :: thesis: verumdL <= x

let x be Element of (subrelstr S); :: thesis: ( x in the carrier of (subrelstr S) implies dL <= x )

assume x in the carrier of (subrelstr S) ; :: thesis: dL <= x

reconsider x1 = x as Element of L by YELLOW_0:58;

Bottom L <= x1 by YELLOW_0:44;

hence dL <= x by YELLOW_0:60; :: thesis: verum

end;assume x in the carrier of (subrelstr S) ; :: thesis: dL <= x

reconsider x1 = x as Element of L by YELLOW_0:58;

Bottom L <= x1 by YELLOW_0:44;

hence dL <= x by YELLOW_0:60; :: thesis: verum