let U be non empty set ; 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; ( A c= B implies Inter (A,B) is non empty ordered Subset-Family of U )
assume A1:
A c= B
; 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; verum