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