let U be non empty set ; :: thesis: for A, B being Subset of U st A c= B holds
Inter A,B is non empty ordered Subset-Family of U
let A, B be Subset of U; :: thesis: ( A c= B implies Inter A,B is non empty ordered Subset-Family of U )
assume a: A c= B ; :: thesis: Inter A,B is non empty ordered Subset-Family of U
consider C, D being set such that
a2: ( C = A & D = B ) ;
( C in Inter A,B & D in Inter A,B & ( for Y being set holds
( Y in Inter A,B iff ( C c= Y & Y c= D ) ) ) ) by a2, Lemacik, a;
hence Inter A,B is non empty ordered Subset-Family of U by DefOr; :: thesis: verum