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 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;
hence ( Y in A iff ( min A c= Y & Y c= max A ) ) by Lm2, Lm3; :: thesis: verum