let S be non empty RelStr ; :: thesis: for D1, D2 being Subset of S holds () .: [:D1,D2:] = D1 "\/" D2
let D1, D2 be Subset of S; :: thesis: () .: [: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= () .: [:D1,D2:]
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in () .: [:D1,D2:] or q in D1 "\/" D2 )
assume A1: q in () .: [: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 = () . c by ;
consider x, y being object such that
A4: ( x in D1 & y in D2 ) and
A5: c = [x,y] by ;
reconsider x = x, y = y as Element of S by A4;
q = () . (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 object ; :: according to TARSKI:def 3 :: thesis: ( not q in D1 "\/" D2 or q in () .: [:D1,D2:] )
assume q in D1 "\/" D2 ; :: thesis: q in () .: [: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 = () . (x,y) & [x,y] in X ) by ;
hence q in () .: [:D1,D2:] by FUNCT_2:35; :: thesis: verum