let L be non empty RelStr ; :: thesis: for S being Subset of L holds

( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S )

let S be Subset of L; :: thesis: ( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S )

thus ( S is meet-closed implies for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S ) :: thesis: ( ( for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S ) implies S is meet-closed )

inf {x,y} in S ; :: thesis: S is meet-closed

hence S is meet-closed ; :: thesis: verum

( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S )

let S be Subset of L; :: thesis: ( S is meet-closed iff for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S )

thus ( S is meet-closed implies for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S ) :: thesis: ( ( for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S ) implies S is meet-closed )

proof

assume A5:
for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds
assume
S is meet-closed
; :: thesis: for x, y being Element of L st x in S & y in S & ex_inf_of {x,y},L holds

inf {x,y} in S

then A1: subrelstr S is meet-inheriting ;

let x, y be Element of L; :: thesis: ( x in S & y in S & ex_inf_of {x,y},L implies inf {x,y} in S )

assume that

A2: x in S and

A3: y in S and

A4: ex_inf_of {x,y},L ; :: thesis: inf {x,y} in S

the carrier of (subrelstr S) = S by YELLOW_0:def 15;

hence inf {x,y} in S by A1, A2, A3, A4; :: thesis: verum

end;inf {x,y} in S

then A1: subrelstr S is meet-inheriting ;

let x, y be Element of L; :: thesis: ( x in S & y in S & ex_inf_of {x,y},L implies inf {x,y} in S )

assume that

A2: x in S and

A3: y in S and

A4: ex_inf_of {x,y},L ; :: thesis: inf {x,y} in S

the carrier of (subrelstr S) = S by YELLOW_0:def 15;

hence inf {x,y} in S by A1, A2, A3, A4; :: thesis: verum

inf {x,y} in S ; :: thesis: S is meet-closed

now :: thesis: for x, y being Element of L st x in the carrier of (subrelstr S) & y in the carrier of (subrelstr S) & ex_inf_of {x,y},L holds

inf {x,y} in the carrier of (subrelstr S)

then
subrelstr S is meet-inheriting
;inf {x,y} in the carrier of (subrelstr S)

let x, y be Element of L; :: thesis: ( x in the carrier of (subrelstr S) & y in the carrier of (subrelstr S) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (subrelstr S) )

assume that

A6: x in the carrier of (subrelstr S) and

A7: y in the carrier of (subrelstr S) and

A8: ex_inf_of {x,y},L ; :: thesis: inf {x,y} in the carrier of (subrelstr S)

the carrier of (subrelstr S) = S by YELLOW_0:def 15;

hence inf {x,y} in the carrier of (subrelstr S) by A5, A6, A7, A8; :: thesis: verum

end;assume that

A6: x in the carrier of (subrelstr S) and

A7: y in the carrier of (subrelstr S) and

A8: ex_inf_of {x,y},L ; :: thesis: inf {x,y} in the carrier of (subrelstr S)

the carrier of (subrelstr S) = S by YELLOW_0:def 15;

hence inf {x,y} in the carrier of (subrelstr S) by A5, A6, A7, A8; :: thesis: verum

hence S is meet-closed ; :: thesis: verum