let L be non empty antisymmetric RelStr ; :: thesis: ( ( L is with_suprema or L is with_infima ) implies for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds

X /\ Y is filtered )

assume A1: ( L is with_suprema or L is with_infima ) ; :: thesis: for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds

X /\ Y is filtered

let X, Y be Subset of L; :: thesis: ( X is upper & X is filtered & Y is upper & Y is filtered implies X /\ Y is filtered )

assume that

A2: ( X is upper & X is filtered ) and

A3: ( Y is upper & Y is filtered ) ; :: thesis: X /\ Y is filtered

A4: X /\ Y is upper by A2, A3, Th29;

X /\ Y is filtered )

assume A1: ( L is with_suprema or L is with_infima ) ; :: thesis: for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds

X /\ Y is filtered

let X, Y be Subset of L; :: thesis: ( X is upper & X is filtered & Y is upper & Y is filtered implies X /\ Y is filtered )

assume that

A2: ( X is upper & X is filtered ) and

A3: ( Y is upper & Y is filtered ) ; :: thesis: X /\ Y is filtered

A4: X /\ Y is upper by A2, A3, Th29;

per cases
( L is with_infima or L is with_suprema )
by A1;

end;

suppose A5:
L is with_infima
; :: thesis: X /\ Y is filtered

end;

now :: thesis: for x, y being Element of L st x in X /\ Y & y in X /\ Y holds

x "/\" y in X /\ Y

hence
X /\ Y is filtered
by A4, A5, Th41; :: thesis: verumx "/\" y in X /\ Y

let x, y be Element of L; :: thesis: ( x in X /\ Y & y in X /\ Y implies x "/\" y in X /\ Y )

assume that

A6: x in X /\ Y and

A7: y in X /\ Y ; :: thesis: x "/\" y in X /\ Y

A8: x in X by A6, XBOOLE_0:def 4;

A9: x in Y by A6, XBOOLE_0:def 4;

A10: y in X by A7, XBOOLE_0:def 4;

A11: y in Y by A7, XBOOLE_0:def 4;

A12: x "/\" y in X by A2, A5, A8, A10, Th41;

x "/\" y in Y by A3, A5, A9, A11, Th41;

hence x "/\" y in X /\ Y by A12, XBOOLE_0:def 4; :: thesis: verum

end;assume that

A6: x in X /\ Y and

A7: y in X /\ Y ; :: thesis: x "/\" y in X /\ Y

A8: x in X by A6, XBOOLE_0:def 4;

A9: x in Y by A6, XBOOLE_0:def 4;

A10: y in X by A7, XBOOLE_0:def 4;

A11: y in Y by A7, XBOOLE_0:def 4;

A12: x "/\" y in X by A2, A5, A8, A10, Th41;

x "/\" y in Y by A3, A5, A9, A11, Th41;

hence x "/\" y in X /\ Y by A12, XBOOLE_0:def 4; :: thesis: verum

suppose A13:
L is with_suprema
; :: thesis: X /\ Y is filtered

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( x in X /\ Y & y in X /\ Y implies ex z being Element of L st

( z in X /\ Y & z <= x & z <= y ) )

assume that

A14: x in X /\ Y and

A15: y in X /\ Y ; :: thesis: ex z being Element of L st

( z in X /\ Y & z <= x & z <= y )

A16: x in X by A14, XBOOLE_0:def 4;

A17: x in Y by A14, XBOOLE_0:def 4;

A18: y in X by A15, XBOOLE_0:def 4;

A19: y in Y by A15, XBOOLE_0:def 4;

consider zx being Element of L such that

A20: zx in X and

A21: x >= zx and

A22: y >= zx by A2, A16, A18;

consider zy being Element of L such that

A23: zy in Y and

A24: x >= zy and

A25: y >= zy by A3, A17, A19;

take z = zx "\/" zy; :: thesis: ( z in X /\ Y & z <= x & z <= y )

A26: z >= zx by A13, YELLOW_0:22;

A27: z >= zy by A13, YELLOW_0:22;

A28: z in X by A2, A20, A26;

z in Y by A3, A23, A27;

hence z in X /\ Y by A28, XBOOLE_0:def 4; :: thesis: ( z <= x & z <= y )

thus ( z <= x & z <= y ) by A13, A21, A22, A24, A25, YELLOW_0:22; :: thesis: verum

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

assume that

A14: x in X /\ Y and

A15: y in X /\ Y ; :: thesis: ex z being Element of L st

( z in X /\ Y & z <= x & z <= y )

A16: x in X by A14, XBOOLE_0:def 4;

A17: x in Y by A14, XBOOLE_0:def 4;

A18: y in X by A15, XBOOLE_0:def 4;

A19: y in Y by A15, XBOOLE_0:def 4;

consider zx being Element of L such that

A20: zx in X and

A21: x >= zx and

A22: y >= zx by A2, A16, A18;

consider zy being Element of L such that

A23: zy in Y and

A24: x >= zy and

A25: y >= zy by A3, A17, A19;

take z = zx "\/" zy; :: thesis: ( z in X /\ Y & z <= x & z <= y )

A26: z >= zx by A13, YELLOW_0:22;

A27: z >= zy by A13, YELLOW_0:22;

A28: z in X by A2, A20, A26;

z in Y by A3, A23, A27;

hence z in X /\ Y by A28, XBOOLE_0:def 4; :: thesis: ( z <= x & z <= y )

thus ( z <= x & z <= y ) by A13, A21, A22, A24, A25, YELLOW_0:22; :: thesis: verum