let x, Y be set ; :: thesis: for A being Subset of Y st x in A holds
(incl A) . x in Y
let A be Subset of Y; :: thesis: ( x in A implies (incl A) . x in Y )
assume A1: x in A ; :: thesis: (incl A) . x in Y
( dom (incl A) = A & rng (incl A) = A ) ;
then (incl A) . x in A by A1, FUNCT_1:def 3;
hence (incl A) . x in Y ; :: thesis: verum