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 a0: 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 KonceWInter, Lemacik;
then c1: A = min F by DefMi;
( B is Element of F & ( for Y being set st Y in F holds
Y c= B ) ) by KonceWInter, a0, Lemacik;
hence ( min F = A & max F = B ) by c1, DefMa; :: thesis: verum