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 object ; :: 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 object such that
x in dom (sup F) and
A1: x in D and
A2: a = (sup F) . x by FUNCT_1:def 6;
reconsider x9 = x as Element of S by A1;
a = "\/" ( { (f . x9) where f is Element of (T |^ the carrier of S) : f in F } ,T) by A2, 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

sup F is Function of S,T by Th6;
then A3: dom (sup F) = the carrier of S by FUNCT_2:def 1;
let a be object ; :: 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
A4: ( a = "\/" ( { (f . i1) where f is Element of (T |^ the carrier of S) : f in F } ,T) & i1 in D ) ;
a = (sup F) . i1 by A4, Th25;
hence a in (sup F) .: D by A4, A3, FUNCT_1:def 6; :: thesis: verum

end;