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:]

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

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 D1 "/\" D2 or q in (inf_op S) .: [:D1,D2:] )
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;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

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