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;
reconsider X = [:D1,D2:] as set ;
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:] and
A3: q1 = (sup_op S) . c by A1, FUNCT_2:65;
consider x, y being set such that
A4: ( x in D1 & y in D2 ) and
A5: c = [x,y] by A2, ZFMISC_1:def 2;
reconsider x = x, y = y as Element of S by A4;
q = (sup_op S) . (x,y) by A3, A5
.= x "\/" y by Def5 ;
then q in { (a "\/" b) where a, b is Element of S : ( a in D1 & b in D2 ) } by A4;
hence q in D1 "\/" D2 by YELLOW_4:def 3; :: thesis: verum

end;

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
A6: ( q = x "\/" y & x in D1 & y in D2 ) ;
( q = (sup_op S) . (x,y) & [x,y] in X ) by A6, Def5, ZFMISC_1:87;
hence q in (sup_op S) .: [:D1,D2:] by FUNCT_2:35; :: thesis: verum