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 A1: 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, Th1, A1;

hence Inter (A,B) is non empty ordered Subset-Family of U by Def8; :: thesis: verum

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 A1: 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, Th1, A1;

hence Inter (A,B) is non empty ordered Subset-Family of U by Def8; :: thesis: verum