let L be non empty transitive RelStr ; :: thesis: for S being non empty meet-closed Subset of L

for x, y being Element of S st ex_inf_of {x,y},L holds

( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )

let S be non empty meet-closed Subset of L; :: thesis: for x, y being Element of S st ex_inf_of {x,y},L holds

( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )

let x, y be Element of S; :: thesis: ( ex_inf_of {x,y},L implies ( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) ) )

A1: x is Element of (subrelstr S) by YELLOW_0:def 15;

A2: y is Element of (subrelstr S) by YELLOW_0:def 15;

assume A3: ex_inf_of {x,y},L ; :: thesis: ( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )

subrelstr S is non empty full meet-inheriting SubRelStr of L by Def1;

then "/\" ({x,y},L) in the carrier of (subrelstr S) by A1, A2, A3, YELLOW_0:def 16;

hence ( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) ) by A1, A2, A3, YELLOW_0:65; :: thesis: verum

for x, y being Element of S st ex_inf_of {x,y},L holds

( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )

let S be non empty meet-closed Subset of L; :: thesis: for x, y being Element of S st ex_inf_of {x,y},L holds

( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )

let x, y be Element of S; :: thesis: ( ex_inf_of {x,y},L implies ( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) ) )

A1: x is Element of (subrelstr S) by YELLOW_0:def 15;

A2: y is Element of (subrelstr S) by YELLOW_0:def 15;

assume A3: ex_inf_of {x,y},L ; :: thesis: ( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )

subrelstr S is non empty full meet-inheriting SubRelStr of L by Def1;

then "/\" ({x,y},L) in the carrier of (subrelstr S) by A1, A2, A3, YELLOW_0:def 16;

hence ( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) ) by A1, A2, A3, YELLOW_0:65; :: thesis: verum