let S be non empty RelStr ; :: thesis: for T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for D being non empty Subset of S holds (sup F) .: D = { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D }
let T be complete LATTICE; :: thesis: for F being non empty Subset of (T |^ the carrier of S)
for D being non empty Subset of S holds (sup F) .: D = { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D }
let F be non empty Subset of (T |^ the carrier of S); :: thesis: for D being non empty Subset of S holds (sup F) .: D = { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D }
let D be non empty Subset of S; :: thesis: (sup F) .: D = { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D }
thus (sup F) .: D c= { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D } :: according to XBOOLE_0:def 10 :: thesis: { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D } c= (sup F) .: D

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (sup F) .: D or a in { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D } )
assume a in (sup F) .: D ; :: thesis: a in { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D }
then consider x being set such that
A1: ( x in dom (sup F) & x in D & a = (sup F) . x ) by FUNCT_1:def 12;
reconsider x' = x as Element of S by A1;
a = "\/" { (f . x') where f is Element of (T |^ the carrier of S) : f in F } ,T by A1, Th25;
hence a in { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D } by A1; :: thesis: verum

end;

thus { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D } c= (sup F) .: D :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D } or a in (sup F) .: D )
assume a in { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D } ; :: thesis: a in (sup F) .: D
then consider i1 being Element of S such that
A2: ( a = "\/" { (f . i1) where f is Element of (T |^ the carrier of S) : f in F } ,T & i1 in D ) ;
A3: a = (sup F) . i1 by A2, Th25;
sup F is Function of S,T by Th6;
then dom (sup F) = the carrier of S by FUNCT_2:def 1;
hence a in (sup F) .: D by A2, A3, FUNCT_1:def 12; :: thesis: verum

end;