let R be non empty Poset; :: thesis: for A being ManySortedSet of the carrier of R
for s being Element of R
for x being set st x in A . s holds
x in A -carrier_of (CComp s)
let A be ManySortedSet of the carrier of R; :: thesis: for s being Element of R
for x being set st x in A . s holds
x in A -carrier_of (CComp s)
let s be Element of R; :: thesis: for x being set st x in A . s holds
x in A -carrier_of (CComp s)
let x be set ; :: thesis: ( x in A . s implies x in A -carrier_of (CComp s) )
assume A1: x in A . s ; :: thesis: x in A -carrier_of (CComp s)
s in CComp s by EQREL_1:20;
then A . s in { (A . s1) where s1 is Element of R : s1 in CComp s } ;
hence x in A -carrier_of (CComp s) by A1, TARSKI:def 4; :: thesis: verum