let S be non empty RelStr ; :: thesis: for D1, D2 being Subset of S holds (sup_op S) .: [:D1,D2:] = D1 "\/" D2
let D1, D2 be Subset of S; :: thesis: (sup_op S) .: [:D1,D2:] = D1 "\/" D2
set f = sup_op S;
thus (sup_op S) .: [:D1,D2:] c= D1 "\/" D2 :: according to XBOOLE_0:def 10 :: thesis: D1 "\/" D2 c= (sup_op S) .: [:D1,D2:]

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in (sup_op S) .: [:D1,D2:] or q in D1 "\/" D2 )
assume A1: q in (sup_op S) .: [:D1,D2:] ; :: thesis: q in D1 "\/" D2
then reconsider q1 = q as Element of S ;
consider c being Element of [:S,S:] such that
A2: ( c in [:D1,D2:] & q1 = (sup_op S) . c ) by A1, FUNCT_2:116;
consider x, y being set such that
A3: ( x in D1 & y in D2 & c = [x,y] ) by A2, ZFMISC_1:def 2;
reconsider x = x, y = y as Element of S by A3;
q = (sup_op S) . x,y by A2, A3
.= x "\/" y by Def5 ;
then q in { (a "\/" b) where a, b is Element of S : ( a in D1 & b in D2 ) } by A3;
hence q in D1 "\/" D2 by YELLOW_4:def 3; :: thesis: verum

end;

reconsider X = [:D1,D2:] as set ;
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in D1 "\/" D2 or q in (sup_op S) .: [:D1,D2:] )
assume q in D1 "\/" D2 ; :: thesis: q in (sup_op S) .: [:D1,D2:]
then q in { (x "\/" y) where x, y is Element of S : ( x in D1 & y in D2 ) } by YELLOW_4:def 3;
then consider x, y being Element of S such that
A4: ( q = x "\/" y & x in D1 & y in D2 ) ;
A5: q = (sup_op S) . x,y by A4, Def5;
[x,y] in X by A4, ZFMISC_1:106;
hence q in (sup_op S) .: [:D1,D2:] by A5, FUNCT_2:43; :: thesis: verum