let R be non empty 1-sorted ; :: thesis: for X being Subset of R holds { x where x is Element of R : {} c= X } = [#] R
let X be Subset of R; :: thesis: { x where x is Element of R : {} c= X } = [#] R
thus { x where x is Element of R : {} c= X } c= [#] R :: according to XBOOLE_0:def 10 :: thesis: [#] R c= { x where x is Element of R : {} c= X }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of R : {} c= X } or y in [#] R )
assume y in { x where x is Element of R : {} c= X } ; :: thesis: y in [#] R
then ex z being Element of R st
( z = y & {} c= X ) ;
hence y in [#] R ; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [#] R or y in { x where x is Element of R : {} c= X } )
assume A1: y in [#] R ; :: thesis: y in { x where x is Element of R : {} c= X }
y in { x where x is Element of R : {} c= X }
proof
assume not y in { x where x is Element of R : {} c= X } ; :: thesis: contradiction
then ( not y is Element of R or not {} c= X ) ;
hence contradiction by A1; :: thesis: verum
end;
hence y in { x where x is Element of R : {} c= X } ; :: thesis: verum