set X = [:D1,D2:];
[:D1,D2:] is filtered
proof
let x,
y be
Element of
[:S1,S2:];
WAYBEL_0:def 2 ( not x in [:D1,D2:] or not y in [:D1,D2:] or ex b1 being Element of the carrier of [:S1,S2:] st
( b1 in [:D1,D2:] & b1 <= x & b1 <= y ) )
assume that A1:
x in [:D1,D2:]
and A2:
y in [:D1,D2:]
;
ex b1 being Element of the carrier of [:S1,S2:] st
( b1 in [:D1,D2:] & b1 <= x & b1 <= y )
consider x1,
x2 being
object such that A3:
x1 in D1
and A4:
x2 in D2
and A5:
x = [x1,x2]
by A1, ZFMISC_1:def 2;
reconsider S29 =
S2 as non
empty RelStr by A4;
reconsider S19 =
S1 as non
empty RelStr by A3;
consider y1,
y2 being
object such that A6:
y1 in D1
and A7:
y2 in D2
and A8:
y = [y1,y2]
by A2, ZFMISC_1:def 2;
reconsider x2 =
x2,
y2 =
y2 as
Element of
S2 by A4, A7;
consider xy2 being
Element of
S2 such that A9:
xy2 in D2
and A10:
(
x2 >= xy2 &
y2 >= xy2 )
by A4, A7, WAYBEL_0:def 2;
reconsider x1 =
x1,
y1 =
y1 as
Element of
S1 by A3, A6;
consider xy1 being
Element of
S1 such that A11:
xy1 in D1
and A12:
(
x1 >= xy1 &
y1 >= xy1 )
by A3, A6, WAYBEL_0:def 2;
reconsider xy29 =
xy2 as
Element of
S29 ;
reconsider xy19 =
xy1 as
Element of
S19 ;
[xy19,xy29] is
Element of
[:S19,S29:]
;
then reconsider z =
[xy1,xy2] as
Element of
[:S1,S2:] ;
take
z
;
( z in [:D1,D2:] & z <= x & z <= y )
thus
z in [:D1,D2:]
by A11, A9, ZFMISC_1:87;
( z <= x & z <= y )
( not
S1 is
empty & not
S2 is
empty )
by A3, A4;
hence
(
z <= x &
z <= y )
by A5, A8, A12, A10, Th11;
verum
end;
hence
for b1 being Subset of [:S1,S2:] st b1 = [:D1,D2:] holds
b1 is filtered
; verum