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