let Y be non empty set ; :: thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))
let a, b, c be Function of Y,BOOLEAN; :: thesis: ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))
let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a))) . z = TRUE or (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE )
A1: (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a))) . z = (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) . z) '&' ((c 'or' ('not' a)) . z) by MARGREL1:def 20
.= (((a 'or' ('not' b)) . z) '&' ((b 'or' ('not' c)) . z)) '&' ((c 'or' ('not' a)) . z) by MARGREL1:def 20
.= (((a . z) 'or' (('not' b) . z)) '&' ((b 'or' ('not' c)) . z)) '&' ((c 'or' ('not' a)) . z) by BVFUNC_1:def 4
.= (((a . z) 'or' (('not' b) . z)) '&' ((b . z) 'or' (('not' c) . z))) '&' ((c 'or' ('not' a)) . z) by BVFUNC_1:def 4
.= (((a . z) 'or' (('not' b) . z)) '&' ((b . z) 'or' (('not' c) . z))) '&' ((c . z) 'or' (('not' a) . z)) by BVFUNC_1:def 4
.= (((a . z) 'or' ('not' (b . z))) '&' ((b . z) 'or' (('not' c) . z))) '&' ((c . z) 'or' (('not' a) . z)) by MARGREL1:def 19
.= (((a . z) 'or' ('not' (b . z))) '&' ((b . z) 'or' ('not' (c . z)))) '&' ((c . z) 'or' (('not' a) . z)) by MARGREL1:def 19
.= (((a . z) 'or' ('not' (b . z))) '&' ((b . z) 'or' ('not' (c . z)))) '&' ((c . z) 'or' ('not' (a . z))) by MARGREL1:def 19 ;
assume A2: (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a))) . z = TRUE ; :: thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE

now :: thesis: ( (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z <> TRUE implies (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE )

A3: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) . z) '&' ((a 'or' ('not' c)) . z) by MARGREL1:def 20
.= (((b 'or' ('not' a)) . z) '&' ((c 'or' ('not' b)) . z)) '&' ((a 'or' ('not' c)) . z) by MARGREL1:def 20
.= (((b . z) 'or' (('not' a) . z)) '&' ((c 'or' ('not' b)) . z)) '&' ((a 'or' ('not' c)) . z) by BVFUNC_1:def 4
.= (((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z))) '&' ((a 'or' ('not' c)) . z) by BVFUNC_1:def 4
.= (((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z))) '&' ((a . z) 'or' (('not' c) . z)) by BVFUNC_1:def 4 ;
assume A4: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z <> TRUE ; :: thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE

now :: thesis: ( ( ((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z)) = FALSE & (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ) or ( (a . z) 'or' (('not' c) . z) = FALSE & (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ) )

per cases ( ((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z)) = FALSE or (a . z) 'or' (('not' c) . z) = FALSE ) by A4, A3, MARGREL1:12, XBOOLEAN:def 3;

case A5: ((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z)) = FALSE ; :: thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE

now :: thesis: ( ( (b . z) 'or' (('not' a) . z) = FALSE & (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ) or ( (c . z) 'or' (('not' b) . z) = FALSE & (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ) )

per cases ( (b . z) 'or' (('not' a) . z) = FALSE or (c . z) 'or' (('not' b) . z) = FALSE ) by A5, MARGREL1:12;

case A6: (b . z) 'or' (('not' a) . z) = FALSE ; :: thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE

A7: ( ('not' a) . z = TRUE or ('not' a) . z = FALSE ) by XBOOLEAN:def 3;
then 'not' (a . z) = FALSE by A6, MARGREL1:def 19;
hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE by A2, A1, A6, A7, XBOOLEAN:138; :: thesis: verum

end;

case A8: (c . z) 'or' (('not' b) . z) = FALSE ; :: thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE

A9: ( ('not' b) . z = TRUE or ('not' b) . z = FALSE ) by XBOOLEAN:def 3;
then 'not' (b . z) = FALSE by A8, MARGREL1:def 19;
hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE by A2, A1, A8, A9, XBOOLEAN:138; :: thesis: verum

end;

end;

end;

hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ; :: thesis: verum

end;

case A10: (a . z) 'or' (('not' c) . z) = FALSE ; :: thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE

A11: ( ('not' c) . z = TRUE or ('not' c) . z = FALSE ) by XBOOLEAN:def 3;
then 'not' (c . z) = FALSE by A10, MARGREL1:def 19;
hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE by A2, A1, A10, A11, XBOOLEAN:138; :: thesis: verum

end;

end;

end;

hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ; :: thesis: verum

end;

hence (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ; :: thesis: verum