let U be non empty set ; :: thesis: for A, B being Subset of U

for F being non empty ordered Subset-Family of U st F = Inter (A,B) holds

( min F = A & max F = B )

let A, B be Subset of U; :: thesis: for F being non empty ordered Subset-Family of U st F = Inter (A,B) holds

( min F = A & max F = B )

let F be non empty ordered Subset-Family of U; :: thesis: ( F = Inter (A,B) implies ( min F = A & max F = B ) )

assume A1: F = Inter (A,B) ; :: thesis: ( min F = A & max F = B )

then ( A is Element of F & ( for Y being set st Y in F holds

A c= Y ) ) by Th2, Th1;

then A2: A = min F by Lm2;

( B is Element of F & ( for Y being set st Y in F holds

Y c= B ) ) by Th2, A1, Th1;

hence ( min F = A & max F = B ) by A2, Lm3; :: thesis: verum

for F being non empty ordered Subset-Family of U st F = Inter (A,B) holds

( min F = A & max F = B )

let A, B be Subset of U; :: thesis: for F being non empty ordered Subset-Family of U st F = Inter (A,B) holds

( min F = A & max F = B )

let F be non empty ordered Subset-Family of U; :: thesis: ( F = Inter (A,B) implies ( min F = A & max F = B ) )

assume A1: F = Inter (A,B) ; :: thesis: ( min F = A & max F = B )

then ( A is Element of F & ( for Y being set st Y in F holds

A c= Y ) ) by Th2, Th1;

then A2: A = min F by Lm2;

( B is Element of F & ( for Y being set st Y in F holds

Y c= B ) ) by Th2, A1, Th1;

hence ( min F = A & max F = B ) by A2, Lm3; :: thesis: verum