let L be Semilattice; :: thesis: for X being non empty upper Subset of L holds

( X is Filter of L iff subrelstr X is meet-inheriting )

let X be non empty upper Subset of L; :: thesis: ( X is Filter of L iff subrelstr X is meet-inheriting )

set S = subrelstr X;

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

inf {x,y} in the carrier of (subrelstr X) ; :: according to YELLOW_0:def 16 :: thesis: X is Filter of L

X is filtered

( X is Filter of L iff subrelstr X is meet-inheriting )

let X be non empty upper Subset of L; :: thesis: ( X is Filter of L iff subrelstr X is meet-inheriting )

set S = subrelstr X;

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

hereby :: thesis: ( subrelstr X is meet-inheriting implies X is Filter of L )

assume A9:
for x, y being Element of L st x in the carrier of (subrelstr X) & y in the carrier of (subrelstr X) & ex_inf_of {x,y},L holds assume A2:
X is Filter of L
; :: thesis: subrelstr X is meet-inheriting

thus subrelstr X is meet-inheriting :: thesis: verum

end;thus subrelstr X is meet-inheriting :: thesis: verum

proof

let x, y be Element of L; :: according to YELLOW_0:def 16 :: thesis: ( not x in the carrier of (subrelstr X) or not y in the carrier of (subrelstr X) or not ex_inf_of {x,y},L or "/\" ({x,y},L) in the carrier of (subrelstr X) )

assume that

A3: x in the carrier of (subrelstr X) and

A4: y in the carrier of (subrelstr X) and

A5: ex_inf_of {x,y},L ; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr X)

consider z being Element of L such that

A6: z in X and

A7: x >= z and

A8: y >= z by A1, A2, A3, A4, Def2;

z is_<=_than {x,y} by A7, A8, YELLOW_0:8;

then z <= inf {x,y} by A5, YELLOW_0:def 10;

hence "/\" ({x,y},L) in the carrier of (subrelstr X) by A1, A6, Def20; :: thesis: verum

end;assume that

A3: x in the carrier of (subrelstr X) and

A4: y in the carrier of (subrelstr X) and

A5: ex_inf_of {x,y},L ; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr X)

consider z being Element of L such that

A6: z in X and

A7: x >= z and

A8: y >= z by A1, A2, A3, A4, Def2;

z is_<=_than {x,y} by A7, A8, YELLOW_0:8;

then z <= inf {x,y} by A5, YELLOW_0:def 10;

hence "/\" ({x,y},L) in the carrier of (subrelstr X) by A1, A6, Def20; :: thesis: verum

inf {x,y} in the carrier of (subrelstr X) ; :: according to YELLOW_0:def 16 :: thesis: X is Filter of L

X is filtered

proof

hence
X is Filter of L
; :: thesis: verum
let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( x in X & y in X implies ex z being Element of L st

( z in X & z <= x & z <= y ) )

assume that

A10: x in X and

A11: y in X ; :: thesis: ex z being Element of L st

( z in X & z <= x & z <= y )

take z = inf {x,y}; :: thesis: ( z in X & z <= x & z <= y )

A12: z = x "/\" y by YELLOW_0:40;

ex_inf_of {x,y},L by YELLOW_0:21;

hence ( z in X & z <= x & z <= y ) by A1, A9, A10, A11, A12, YELLOW_0:19; :: thesis: verum

end;( z in X & z <= x & z <= y ) )

assume that

A10: x in X and

A11: y in X ; :: thesis: ex z being Element of L st

( z in X & z <= x & z <= y )

take z = inf {x,y}; :: thesis: ( z in X & z <= x & z <= y )

A12: z = x "/\" y by YELLOW_0:40;

ex_inf_of {x,y},L by YELLOW_0:21;

hence ( z in X & z <= x & z <= y ) by A1, A9, A10, A11, A12, YELLOW_0:19; :: thesis: verum