let X, Y be set ; :: thesis: for A being non empty ordered Subset-Family of X holds
( Y in A iff ( min A c= Y & Y c= max A ) )
let A be non empty ordered Subset-Family of X; :: thesis: ( Y in A iff ( min A c= Y & Y c= max A ) )
( min A c= Y & Y c= max A implies Y in A )

proof

assume b1: ( min A c= Y & Y c= max A ) ; :: thesis: Y in A
consider C, D being set such that
b2: ( C in A & D in A & ( for X being set holds
( X in A iff ( C c= X & X c= D ) ) ) ) by DefOr;
XZ: ( min A c= C & D c= max A ) by DefMi, DefMa, b2;
( C c= min A & max A c= D ) by b2;
then ( min A = C & max A = D ) by XZ, XBOOLE_0:def 10;
hence Y in A by b2, b1; :: thesis: verum

end;

hence ( Y in A iff ( min A c= Y & Y c= max A ) ) by DefMi, DefMa; :: thesis: verum