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

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in (inf_op S) .: [:D1,D2:] or q in D1 "/\" D2 )
assume A1: q in (inf_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 = (inf_op S) . c by A1, FUNCT_2:65;
consider x, y being object 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 = (inf_op S) . (x,y) by A3, A5
.= x "/\" y by Def4 ;
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 4; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in D1 "/\" D2 or q in (inf_op S) .: [:D1,D2:] )
assume q in D1 "/\" D2 ; :: thesis: q in (inf_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 4;
then consider x, y being Element of S such that
A6: ( q = x "/\" y & x in D1 & y in D2 ) ;
( q = (inf_op S) . (x,y) & [x,y] in X ) by A6, Def4, ZFMISC_1:87;
hence q in (inf_op S) .: [:D1,D2:] by FUNCT_2:35; :: thesis: verum