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 )

( 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

hence
( Y in A iff ( min A c= Y & Y c= max A ) )
by Lm2, Lm3; :: thesis: verum
assume A1:
( min A c= Y & Y c= max A )
; :: thesis: Y in A

consider C, D being set such that

A2: ( C in A & D in A & ( for X being set holds

( X in A iff ( C c= X & X c= D ) ) ) ) by Def8;

A3: ( min A c= C & D c= max A ) by Lm2, Lm3, A2;

( C c= min A & max A c= D ) by A2;

then ( min A = C & max A = D ) by A3;

hence Y in A by A2, A1; :: thesis: verum

end;consider C, D being set such that

A2: ( C in A & D in A & ( for X being set holds

( X in A iff ( C c= X & X c= D ) ) ) ) by Def8;

A3: ( min A c= C & D c= max A ) by Lm2, Lm3, A2;

( C c= min A & max A c= D ) by A2;

then ( min A = C & max A = D ) by A3;

hence Y in A by A2, A1; :: thesis: verum